Def Profinite.lightProfiniteConeOfHom_π_app'

Modification history

2024-06-11 13:06

Mathlib/Topology/Category/LightProfinite/IsLight.lean

refactor(LightProfinite): redefine light profinite spaces as second countable profinite spaces (#13319) …

Deleted Profinite.lightProfiniteConeOfHom_π_app'View on Github →

2024-03-12 11:06

Mathlib/Topology/Category/LightProfinite/IsLight.lean

feat(LightProfinite): being light is a property of a profinite space (#10391) …

Added Profinite.lightProfiniteConeOfHom_π_app'View on Github →