Commit 2023-08-31 13:03 93e701ca

View on Github →

feat: the atTop filter is countably generated in a second-countable topology (#6864)

Estimated changes

Modified Mathlib/Data/Set/Intervals/Basic.lean

added theorem Set.Ici_eq_singleton_iff_isTop

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.atBot_eq_pure_of_isBot

added theorem Filter.atTop_eq_generate_Ici

added theorem Filter.atTop_eq_generate_of_forall_exists_le

added theorem Filter.atTop_eq_generate_of_not_bddAbove

added theorem Filter.atTop_eq_pure_of_isTop

Modified Mathlib/Order/Filter/Bases.lean

added theorem Filter.isCountablyGenerated_of_subsingleton_mem

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.eq_bot_or_pure_of_subsingleton_mem

added theorem Filter.eq_pure_iff_singleton_mem

added theorem Filter.le_pure_iff_eq_pure

added theorem Filter.mem_generate_of_mem

Modified Mathlib/Topology/Order/Basic.lean