Commit 2023-08-09 19:01 a2c34345

View on Github →

feat(Topology/ExtremallyDisconnected): prove Gleason's theorem (#5634) This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.

Estimated changes

Modified Mathlib/Data/Set/Basic.lean

added theorem Set.nonempty_iff_ne_empty'

added theorem Set.not_nonempty_iff_eq_empty'

Modified Mathlib/Data/Set/Functor.lean

added theorem Set.coe_subset

added theorem Set.eq_univ_of_coe_eq

added theorem Set.image_coe_eq_restrict_image

added theorem Set.mem_coe_of_mem

added theorem Set.mem_of_mem_coe

Modified Mathlib/Topology/Constructions.lean

added theorem IsClosed.trans

added theorem IsOpen.trans

Modified Mathlib/Topology/ExtremallyDisconnected.lean

added theorem ExtremallyDisconnected.disjoint_closure_of_disjoint_IsOpen

added theorem exists_compact_surjective_zorn_subset

added theorem image_subset_closure_compl_image_compl_of_isOpen