Mathlib Changelog
v4
Changelog
About
Github
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