Commit 2024-07-02 14:31 d180e676

View on Github →

refactor(Topology/Category): add CompHausLike.Limits (#13905) This is the first part of the refactor of CompHaus and friends (adding the new API which will eventually be used to redefine the categories of compact Hausdorff spaces, see https://github.com/leanprover-community/mathlib4/pull/12930)

Estimated changes

Modified Mathlib.lean

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

added theorem CompHausLike.Sigma.openEmbedding_ι

added theorem CompHausLike.finitaryExtensive

added def CompHausLike.finiteCoproduct.desc

added theorem CompHausLike.finiteCoproduct.hom_ext

added def CompHausLike.finiteCoproduct.isColimit

added theorem CompHausLike.finiteCoproduct.openEmbedding_ι

added def CompHausLike.finiteCoproduct.ι

added theorem CompHausLike.finiteCoproduct.ι_desc

added theorem CompHausLike.finiteCoproduct.ι_desc_apply

added theorem CompHausLike.finiteCoproduct.ι_injective

added theorem CompHausLike.finiteCoproduct.ι_jointly_surjective

added def CompHausLike.finiteCoproduct

added theorem CompHausLike.hasPullbacksOfInclusions

added def CompHausLike.isTerminalPUnit

added theorem CompHausLike.pullback.condition

added def CompHausLike.pullback.cone

added def CompHausLike.pullback.fst

added theorem CompHausLike.pullback.hom_ext

added def CompHausLike.pullback.isLimit

added def CompHausLike.pullback.lift

added theorem CompHausLike.pullback.lift_fst

added theorem CompHausLike.pullback.lift_snd

added def CompHausLike.pullback.snd

added def CompHausLike.pullback