Commit 2025-09-02 18:25 1c9b13eb

feat(Archive): Kuratowski's closure-complement theorem (incl. sharpness) (#27090) This is the outcome of a course project at Heidelberg University: https://matematiflo.github.io/CompAssistedMath2025/ feat(Topology): Kuratowski's closure-complement theorem "Topology/Kuratowski.lean" proves Kuratowski's closure-complement theorem, which says that if one repeatedly applies the closure and complement operators to a set in a topological space, at most 14 distinct sets can be obtained. feat(Archive/Examples): sharpness of Kuratowski's closure-complement theorem: "Examples/Kuratowski.lean" gives an example of a so-called "14-set" in ℝ, from which exactly 14 distinct sets can be obtained.