Coq中滤子扩展原理的形式化

滤子扩展原理（FEP）断言每个滤子都可以扩展为一个超滤子，这在寻求非主超滤子的过程中起着至关重要的作用。非主超滤子在逻辑、集合论、拓扑、模型论，尤其是代数结构的非标准扩张中有着广泛的应用。由于非主超滤子难以直接构造，源于选择公理的滤子扩展原理在获取它们方面具有重要价值。本文介绍了滤子扩展原理的形式化验证，该验证使用 Coq 证明助手实现，并基于公理化集合论。它提供了关于滤子基、滤子、超滤子等概念的形式化描述。所有相关定理、命题以及滤子扩展原理本身都得到了严格的形式化验证。这项工作为形式化非标准分析和特定的实数理论奠定了基础。