Commit 2023-01-24 09:59 b2c48732

View on Github →

feat: port Order.Filter.Cofinite (#1813)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Filter/Cofinite.lean

added theorem Filter.Tendsto.exists_forall_ge

added theorem Filter.Tendsto.exists_forall_le

added theorem Filter.Tendsto.exists_within_forall_ge

added theorem Filter.Tendsto.exists_within_forall_le

added theorem Filter.atTop_le_cofinite

added def Filter.cofinite

added theorem Filter.comap_cofinite_le

added theorem Filter.coprod_cofinite

added theorem Filter.coprodᵢ_cofinite

added theorem Filter.disjoint_cofinite_left

added theorem Filter.disjoint_cofinite_right

added theorem Filter.eventually_cofinite

added theorem Filter.eventually_cofinite_ne

added theorem Filter.frequently_cofinite_iff_infinite

added theorem Filter.hasBasis_cofinite

added theorem Filter.le_cofinite_iff_compl_singleton_mem

added theorem Filter.le_cofinite_iff_eventually_ne

added theorem Filter.mem_cofinite

added theorem Finset.eventually_cofinite_nmem

added theorem Function.Injective.comap_cofinite_eq

added theorem Function.Injective.nat_tendsto_atTop

added theorem Function.Injective.tendsto_cofinite

added theorem Nat.cofinite_eq_atTop

added theorem Nat.frequently_atTop_iff_infinite

added theorem Set.Finite.compl_mem_cofinite

added theorem Set.Finite.eventually_cofinite_nmem

added theorem Set.infinite_iff_frequently_cofinite