Commit 2023-11-29 17:02 addb4691

View on Github →

feat(Topology, CategoryTheory): define light profinite sets (#8676) We define light profinite sets as structures containing the data of a sequential limit in Profinite.

Estimated changes

Modified Mathlib.lean

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

added def FintypeCat.toLightProfinite

added def LightProfinite'.toLightFunctor

added def LightProfinite'.toProfinite

added structure LightProfinite'

added def LightProfinite.equivSmall

added theorem LightProfinite.ext

added def LightProfinite.fintypeCatToLightProfinite

added def LightProfinite.lightToProfinite

added def LightProfinite.toProfinite

added structure LightProfinite