Commit 2023-11-30 10:58 ee1b50f2

View on Github →

chore(Profinite): allow more universe flexibility in Profinite/CofilteredLimit (#8613) We allow the indexing category for the cofiltered limit in the result Profinite.exists_locallyConstant to live in a smaller universe than our profinite sets.

Estimated changes

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

modified def Profinite.asLimitConeIso

modified def Profinite.isoAsLimitConeLift

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

modified def Profinite.limitCone

modified def Profinite.limitConeIsLimit

Modified Mathlib/Topology/Category/Profinite/CofilteredLimit.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

Modified Mathlib/Topology/Category/Profinite/Product.lean

modified def Profinite.asLimitindexConeIso