Theorem Topology.ClosureCompl.nodup_theFourteen_of_nodup_theClosedSix_of_disjoint

Modification history

2025-09-02 18:25
Archive/Examples/Kuratowski.lean
feat(Archive): Kuratowski's closure-complement theorem (incl. sharpness) (#27090) …
Added Topology.ClosureCompl.nodup_theFourteen_of_nodup_theClosedSix_of_disjointView on Github →