Commit 2024-03-12 11:06 d1d17722

View on Github →

feat(LightProfinite): being light is a property of a profinite space (#10391) This PR defines the class Profinite.IsLight which is the property of a profinite space to have countably many clopens. We prove that such a profinite space gives rise to a LightProfinite, and the underlying profinite space of a LightProfinite is light.

depends on: #10390

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/LightProfinite/IsLight.lean

added theorem Profinite.isLight_of_mono

added def Profinite.lightProfiniteConeOfHom

added def Profinite.lightProfiniteConeOfHom_π_app'

added def Profinite.lightProfiniteConeOfHom_π_app

added def Profinite.lightProfiniteIsLimitOfMono

Modified Mathlib/Topology/DiscreteQuotient.lean

added theorem DiscreteQuotient.comp_finsetClopens

added def DiscreteQuotient.equivFinsetClopens

added theorem DiscreteQuotient.finsetClopens_inj