Commit 2023-06-09 14:11 9f017855

View on Github →

feat: port Topology.Category.Profinite.CofilteredLimit (#4889)

Estimated changes

Modified Mathlib.lean

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

added theorem Profinite.exists_clopen_of_cofiltered

added theorem Profinite.exists_locallyConstant

added theorem Profinite.exists_locallyConstant_fin_two

added theorem Profinite.exists_locallyConstant_finite_aux

added theorem Profinite.exists_locallyConstant_finite_nonempty