Commit 2023-07-27 19:54 f62d8a1c

View on Github →

feat: define the category of extremally disconnected compact Hausdorff spaces (#5761) Basics of the category Stonean of extremally disconnected compact Hausdorff spaces. This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Set/Image.lean

added theorem sigma_mk_preimage_image'

added theorem sigma_mk_preimage_image_eq_self

Created Mathlib/Topology/Category/Stonean/Basic.lean

added def CompHaus.toStonean

added def Stonean.of

added def Stonean.toCompHaus

added def Stonean.toProfinite

added structure Stonean

Created Mathlib/Topology/Category/Stonean/Limits.lean

added def Stonean.finiteCoproduct.cocone

added def Stonean.finiteCoproduct.desc

added theorem Stonean.finiteCoproduct.hom_ext

added def Stonean.finiteCoproduct.isColimit

added def Stonean.finiteCoproduct.ι

added theorem Stonean.finiteCoproduct.ι_desc

added def Stonean.finiteCoproduct

Modified Mathlib/Topology/ExtremallyDisconnected.lean