Commit 2023-12-21 08:37 4cf00954

View on Github →

feat(Topology/Compact): an infinite set has an accumulation point (#9173) Add more versions of this statement. Also remove simp from Filter.disjoint_cofinite_{left,right} as RHS is not much simpler than LHS.

Estimated changes

Modified Mathlib/Order/Filter/Cofinite.lean

added theorem Filter.cofinite_inf_principal_neBot_iff

added theorem Filter.frequently_cofinite_mem_iff_infinite

added theorem Set.Finite.cofinite_inf_principal_compl

added theorem Set.Finite.cofinite_inf_principal_diff

Modified Mathlib/Topology/Compactness/Compact.lean

added theorem Set.Infinite.exists_accPt_cofinite_inf_principal

added theorem Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompact

added theorem Set.Infinite.exists_accPt_of_subset_isCompact

added theorem Set.Infinite.exists_accPt_principal