Commit 2024-07-31 06:44 2c270faa

View on Github →

refactor(Topology/Category): refactor LightProfinite.Basic (#13912) This is the second part of the refactor of CompHaus and friends (refactoring the definition of LightProfinite in terms of CompHausLike, see #12930 for the end result)

Estimated changes

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

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

deleted theorem LightProfinite.coe_comp

deleted theorem LightProfinite.coe_id

deleted def LightProfinite.homeoOfIso

deleted def LightProfinite.isoEquivHomeo

deleted def LightProfinite.isoOfHomeo

deleted theorem LightProfinite.mono_iff_injective

deleted def LightProfinite.of

deleted theorem LightProfinite.toCompHaus_comp_toTop

deleted def LightProfinite.toTopCat

deleted def LightProfinite.toTopCatFullyFaithful

deleted structure LightProfinite

deleted def lightProfiniteToCompHaus

deleted def lightProfiniteToCompHausFullyFaithful

deleted def lightToProfinite

deleted def lightToProfiniteFullyFaithful

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

modified def LightProfinite.pullbackHomeoPullback