Commit 2023-01-24 20:53 a923247d

View on Github →

feat: port Order.Filter.Ultrafilter (#1814)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/Ultrafilter.lean

added theorem Filter.bot_ne_hyperfilter

added theorem Filter.compl_mem_hyperfilter_of_finite

added theorem Filter.exists_ultrafilter_iff

added theorem Filter.forall_neBot_le_iff

added theorem Filter.hyperfilter_le_cofinite

added theorem Filter.iic_pure

added theorem Filter.isAtom_pure

added theorem Filter.le_iff_ultrafilter

added theorem Filter.le_pure_iff'

added theorem Filter.lt_pure_iff

added theorem Filter.mem_hyperfilter_of_finite_compl

added theorem Filter.mem_iff_ultrafilter

added theorem Filter.nmem_hyperfilter_of_finite

added theorem Filter.supᵢ_ultrafilter_le_eq

added theorem Filter.tendsto_iff_ultrafilter

added def Ultrafilter.bind

added theorem Ultrafilter.coe_comap

added theorem Ultrafilter.coe_inj

added theorem Ultrafilter.coe_injective

added theorem Ultrafilter.coe_le_coe

added theorem Ultrafilter.coe_map

added theorem Ultrafilter.coe_pure

added theorem Ultrafilter.comap_inf_principal_neBot_of_image_mem

added theorem Ultrafilter.comap_pure

added theorem Ultrafilter.compl_mem_iff_not_mem

added theorem Ultrafilter.compl_not_mem_iff

added theorem Ultrafilter.diff_mem_iff

added theorem Ultrafilter.disjoint_iff_not_le

added theorem Ultrafilter.empty_not_mem

added theorem Ultrafilter.eq_of_le

added theorem Ultrafilter.eq_pure_of_finite

added theorem Ultrafilter.eq_pure_of_finite_mem

added theorem Ultrafilter.eventually_imp

added theorem Ultrafilter.eventually_not

added theorem Ultrafilter.eventually_or

added theorem Ultrafilter.exists_le

added theorem Ultrafilter.exists_ultrafilter_of_finite_inter_nonempty

added theorem Ultrafilter.ext

added theorem Ultrafilter.finite_bunionᵢ_mem_iff

added theorem Ultrafilter.finite_unionₛ_mem_iff

added theorem Ultrafilter.frequently_iff_eventually

added theorem Ultrafilter.inf_neBot_iff

added theorem Ultrafilter.le_cofinite_or_eq_pure

added theorem Ultrafilter.le_of_inf_neBot'

added theorem Ultrafilter.le_of_inf_neBot

added theorem Ultrafilter.le_sup_iff

added theorem Ultrafilter.map_id'

added theorem Ultrafilter.map_pure

added theorem Ultrafilter.mem_coe

added theorem Ultrafilter.mem_comap

added theorem Ultrafilter.mem_map

added theorem Ultrafilter.mem_or_compl_mem

added theorem Ultrafilter.mem_pure

added theorem Ultrafilter.ne_empty_of_mem

added theorem Ultrafilter.nonempty_of_mem

added def Ultrafilter.ofAtom

added theorem Ultrafilter.ofComapInfPrincipal_eq_of_map

added theorem Ultrafilter.ofComapInfPrincipal_mem

added def Ultrafilter.ofComplNotMemIff

added theorem Ultrafilter.of_coe

added theorem Ultrafilter.of_le

added theorem Ultrafilter.pure_injective

added theorem Ultrafilter.union_mem_iff

added theorem Ultrafilter.unique

added structure Ultrafilter