Mathlib Changelog
v4
Changelog
About
Github
Theorem
Topology.ClosureCompl.ncard_isObtainable_le_fourteen
Modification history
2025-09-02 18:25
Archive/Kuratowski.lean
feat(Archive): Kuratowski's closure-complement theorem (incl. sharpness) (#27090) …
Added
Topology.ClosureCompl.ncard_isObtainable_le_fourteen
View on Github →