This repository provides the formalization of the Filter Extension Principle (FEP).
The dependency order of these files is: mk_structure.v --> mk_theorems.v --> alge_operation.v --> infinite_set.v --> filter.v --> filter_extension.v
mk_structure.v and mk_theorems.v describe the formalization of Morse-Kelley axiomatic set theory.
alge_operation.v includes the addition and multiplication on ω.
infinite_set.v verifies some properties about infinite sets.
filter.v is the formalization of concepts of filters, maximal filters, ultrafilters, principal ultrafilters, non-principal ultrafilters and free ultrafilters, along with some their properties.
filter_extension.v verifies the Filter Extension Principle.