The Kuratowski closure-complement theorem

This file 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.

In another file it will be shown that the maximum can be realized in the real numbers. (A set realizing the maximum is called a 14-set.)

Main definitions

• Topology.ClosureCompl.IsObtainable is the binary inductive predicate saying that a set can be obtained from another using the closure and complement operations.

• Topology.ClosureCompl.theFourteen is an explicit multiset of fourteen sets obtained from a given set using the closure and complement operations.

Main results

• Topology.ClosureCompl.mem_theFourteen_iff_isObtainable: a set t is obtainable by from s if and only if they are in the Multiset theFourteen s.

• Topology.ClosureCompl.ncard_isObtainable_le_fourteen: for an arbitrary set s, there are at most 14 distinct sets that can be obtained from s using the closure and complement operations (the Kuratowski closure-complement theorem).

Notation

• k: the closure of a set.
• i: the interior of a set.
• c: the complement of a set in docstrings; ᶜ is used in the code.

References

• https://en.wikipedia.org/wiki/Kuratowski%27s_closure-complement_problem
• https://web.archive.org/web/20220212062843/http://nzjm.math.auckland.ac.nz/images/6/63/The_Kuratowski_Closure-Complement_Theorem.pdf

inductive Topology.ClosureCompl.IsObtainable {X : Type u_1} [TopologicalSpace X] (s : Set X) : Set X → Prop

IsObtainable s t means that t can be obtained from s by taking closures and complements.

• base {X : Type u_1} [TopologicalSpace X] {s : Set X} : IsObtainable s s
• closure {X : Type u_1} [TopologicalSpace X] {s : Set X} ⦃t : Set X⦄ : IsObtainable s t → IsObtainable s (closure t)
• complement {X : Type u_1} [TopologicalSpace X] {s : Set X} ⦃t : Set X⦄ : IsObtainable s t → IsObtainable s tᶜ

def Topology.ClosureCompl.termK : Lean.ParserDescr

Equations

• Topology.ClosureCompl.termK = Lean.ParserDescr.node `Topology.ClosureCompl.termK 1024 (Lean.ParserDescr.symbol "k")

def Topology.ClosureCompl.termI : Lean.ParserDescr

Equations

• Topology.ClosureCompl.termI = Lean.ParserDescr.node `Topology.ClosureCompl.termI 1024 (Lean.ParserDescr.symbol "i")

theorem Topology.ClosureCompl.kckc_idem {X : Type u_1} [TopologicalSpace X] (s : Set X) : closure (closure (closure (closure sᶜ)ᶜ)ᶜ)ᶜ = closure (closure sᶜ)ᶜ

The function kckc is idempotent: kckckckc s = kckc s for any set s. This is because ckc = i and ki is idempotent.

theorem Topology.ClosureCompl.kckckck_eq_kck {X : Type u_1} [TopologicalSpace X] (s : Set X) : closure (closure (closure (closure s)ᶜ)ᶜ)ᶜ = closure (closure s)ᶜ

Cancelling the first applied complement we obtain kckckck s = kck s for any set s.

def Topology.ClosureCompl.theFourteen {X : Type u_1} [TopologicalSpace X] (s : Set X) : Multiset (Set X)

The at most fourteen sets that are obtainable from s are given by applying id, c, k, ck, kc, ckc, kck, ckck, kckc, ckckc, kckck, ckckck, kckckc, ckckckc to s.

Equations

• One or more equations did not get rendered due to their size.

theorem Topology.ClosureCompl.card_theFourteen {X : Type u_1} [TopologicalSpace X] (s : Set X) : (theFourteen s).card = 14

theFourteen has exactly 14 sets (possibly with repetition) in it.

theorem Topology.ClosureCompl.IsObtainable.mem_theFourteen {X : Type u_1} [TopologicalSpace X] {s t : Set X} (h : IsObtainable s t) : t ∈ theFourteen s

If t is obtainable from s by the closure and complement operations, then it is in the multiset theFourteen s.

theorem Topology.ClosureCompl.mem_theFourteen_iff_isObtainable {X : Type u_1} [TopologicalSpace X] {s t : Set X} : t ∈ theFourteen s ↔ IsObtainable s t

A set t is obtainable by from s if and only if they are in the Multiset theFourteen s.

theorem Topology.ClosureCompl.ncard_isObtainable_le_fourteen {X : Type u_1} [TopologicalSpace X] (s : Set X) : {t : Set X | IsObtainable s t}.ncard ≤ 14

Kuratowski's closure-complement theorem: the number of obtainable sets via closure and complement operations from a single set s is at most 14.