Commit 2025-01-21 12:39 3a74c6cd

View on Github →

chore: split Mathlib.Order.Filter.Ultrafilter (#20848)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/ModelTheory/Satisfiability.lean

Modified Mathlib/ModelTheory/Ultraproducts.lean

Modified Mathlib/Order/Filter/FilterProduct.lean

Modified Mathlib/Order/Filter/Pointwise.lean

Modified Mathlib/Order/Filter/Subsingleton.lean

Created Mathlib/Order/Filter/Ultrafilter/Basic.lean

added theorem Filter.atBot_eq_pure_of_isBot

added theorem Filter.atTop_eq_pure_of_isTop

added theorem Filter.bot_ne_hyperfilter

added theorem Filter.compl_mem_hyperfilter_of_finite

added theorem Filter.hyperfilter_le_cofinite

added theorem Filter.mem_hyperfilter_of_finite_compl

added theorem Filter.nmem_hyperfilter_of_finite

added theorem Filter.tendsto_iff_ultrafilter

added theorem Nat.hyperfilter_le_atTop

added theorem Ultrafilter.eq_pure_of_finite

added theorem Ultrafilter.eq_pure_of_finite_mem

added theorem Ultrafilter.eventually_exists_iff

added theorem Ultrafilter.eventually_exists_mem_iff

added theorem Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty

added theorem Ultrafilter.finite_biUnion_mem_iff

added theorem Ultrafilter.finite_sUnion_mem_iff

added theorem Ultrafilter.le_cofinite_or_eq_pure

Renamed Mathlib/Order/Filter/Ultrafilter.lean to Mathlib/Order/Filter/Ultrafilter/Defs.lean

deleted theorem Filter.atBot_eq_pure_of_isBot

deleted theorem Filter.atTop_eq_pure_of_isTop

deleted theorem Filter.bot_ne_hyperfilter

deleted theorem Filter.compl_mem_hyperfilter_of_finite

deleted theorem Filter.hyperfilter_le_cofinite

deleted theorem Filter.mem_hyperfilter_of_finite_compl

deleted theorem Filter.nmem_hyperfilter_of_finite

deleted theorem Filter.tendsto_iff_ultrafilter

deleted theorem Nat.hyperfilter_le_atTop

deleted theorem Ultrafilter.eq_pure_of_finite

deleted theorem Ultrafilter.eq_pure_of_finite_mem

deleted theorem Ultrafilter.eventually_exists_iff

deleted theorem Ultrafilter.eventually_exists_mem_iff

deleted theorem Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty

deleted theorem Ultrafilter.finite_biUnion_mem_iff

deleted theorem Ultrafilter.finite_sUnion_mem_iff

deleted theorem Ultrafilter.le_cofinite_or_eq_pure

Modified Mathlib/Topology/Defs/Ultrafilter.lean

Modified Mathlib/Topology/Ultrafilter.lean