Commit 2024-07-31 16:34 a3e5a283

View on Github →

refactor(Topology/Category): use CompHausLike API for limits in LightProfinite (#15362)

Estimated changes

Modified Mathlib/Topology/Category/LightProfinite/EffectiveEpi.lean

deleted def LightProfinite.EffectiveEpi.struct

Modified Mathlib/Topology/Category/LightProfinite/Limits.lean

deleted theorem LightProfinite.Sigma.ι_comp_toFiniteCoproduct

deleted def LightProfinite.coproductHomeoCoproduct

deleted def LightProfinite.coproductIsoCoproduct

deleted def LightProfinite.finiteCoproduct.desc

deleted theorem LightProfinite.finiteCoproduct.hom_ext

deleted def LightProfinite.finiteCoproduct.isColimit

deleted def LightProfinite.finiteCoproduct.ι

deleted theorem LightProfinite.finiteCoproduct.ι_desc

deleted theorem LightProfinite.finiteCoproduct.ι_desc_apply

deleted theorem LightProfinite.finiteCoproduct.ι_injective

deleted theorem LightProfinite.finiteCoproduct.ι_jointly_surjective

deleted def LightProfinite.finiteCoproduct

deleted def LightProfinite.isTerminalPUnit

deleted theorem LightProfinite.pullback.condition

deleted def LightProfinite.pullback.cone

deleted def LightProfinite.pullback.fst

deleted theorem LightProfinite.pullback.hom_ext

deleted def LightProfinite.pullback.isLimit

deleted def LightProfinite.pullback.lift

deleted theorem LightProfinite.pullback.lift_fst

deleted theorem LightProfinite.pullback.lift_snd

deleted def LightProfinite.pullback.snd

deleted def LightProfinite.pullback

deleted def LightProfinite.pullbackHomeoPullback

deleted def LightProfinite.pullbackIsoPullback

deleted theorem LightProfinite.pullback_fst_eq

deleted theorem LightProfinite.pullback_snd_eq