Def LightProfinite'.toLightFunctor

Modification history

2024-06-11 13:06

Mathlib/Topology/Category/LightProfinite/Basic.lean

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

Deleted LightProfinite'.toLightFunctor View on Github →

2023-11-29 17:02

Mathlib/Topology/Category/LightProfinite/Basic.lean

feat(Topology, CategoryTheory): define light profinite sets (#8676) …

Added LightProfinite'.toLightFunctor View on Github →