Kuratowski's closure-complement theorem is sharp

Kuratowski's closure-complement theorem 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.

This file gives an example of a so-called "14-set" in ℝ, from which exactly 14 distinct sets can be obtained.

Our strategy is to show there is no duplication within the fourteen sets obtained from this set s: the fourteen sets can be decomposed into six closed sets, six open sets that are the complements of the closed sets, and s and sᶜ which are neither closed nor open. This reduces 14*13/2 = 91 inequalities to check down to 6*5/2 = 15 inequalities. We'll further show that the 15 inequalities follow from a subset of 6 by algebra.

There are charaterizations and criteria for a set to be a 14-set in the paper "Characterization of Kuratowski 14-Sets" by Eric Langford which we do not formalize.

Main definitions

• Topology.ClosureCompl.fourteenSet: an explicit example of a 14-set in ℝ.
• Topology.ClosureCompl.theClosedSix: the six open sets obtainable from a given set.
• Topology.ClosureCompl.theOpenSix: the six open sets obtainable from a given set.
• Topology.ClosureCompl.TheSixIneq: six inequalities that suffice to deduce that the six closed sets obtained from a given set contain no duplicates.

Main results

• Topology.ClosureCompl.nodup_theFourteen_fourteenSet: the application of all 14 operations on the defined fourteenSet in ℝ gives no duplicates.

• Topology.ClosureCompl.ncard_isObtainable_fourteenSet: for the defined fourteenSet in ℝ, there are exactly 14 distinct sets that can be obtained from fourteenSet using the closure and complement operations.

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

The six closed sets obtained from a given set s are given by applying k, kc, kck, kckc, kckck, kckckc to s.

Equations

• Topology.ClosureCompl.theClosedSix s = {closure s, closure sᶜ, closure (closure s)ᶜ, closure (closure sᶜ)ᶜ, closure (closure (closure s)ᶜ)ᶜ, closure (closure (closure sᶜ)ᶜ)ᶜ}

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

The complements of the six closed sets.

Equations

• Topology.ClosureCompl.theOpenSix s = Multiset.map compl (Topology.ClosureCompl.theClosedSix s)

theorem Topology.ClosureCompl.sum_map_theClosedSix_add_compl {X : Type u_1} [TopologicalSpace X] (s : Set X) : (Multiset.map (fun (t : Set X) => {t} + {tᶜ}) (theClosedSix s)).sum = theClosedSix s + theOpenSix s

theorem Topology.ClosureCompl.theFourteen_eq_pair_add_theClosedSix_add_theOpenSix {X : Type u_1} [TopologicalSpace X] (s : Set X) : theFourteen s = {s, sᶜ} + theClosedSix s + theOpenSix s

theFourteen s can be splitted into 3 subsets.

theorem Topology.ClosureCompl.isClosed_of_mem_theClosedSix {X : Type u_1} [TopologicalSpace X] {s t : Set X} (h : t ∈ theClosedSix s) : IsClosed t

Every set in theClosedSix s is closed (because the last operation is closure).

theorem Topology.ClosureCompl.isOpen_of_mem_theOpenSix {X : Type u_1} [TopologicalSpace X] {s t : Set X} (h : t ∈ theOpenSix s) : IsOpen t

Every set in theOpenSix s is open.

theorem Topology.ClosureCompl.mem_theOpenSix_iff {X : Type u_1} [TopologicalSpace X] {s t : Set X} : t ∈ theOpenSix s ↔ tᶜ ∈ theClosedSix s

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

Six inequalities that suffice to deduce the six closed sets obtained from a given set contain no duplicates.

Equations

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

theorem Topology.ClosureCompl.nodup_theClosedSix_theFourteen_iff {X : Type u_1} [TopologicalSpace X] {s : Set X} : (theClosedSix s).Nodup ↔ TheSixIneq s

theClosedSix applied to an arbitrary set s results in no duplicates iff TheSixIneq is true for s.

theorem Topology.ClosureCompl.nodup_theFourteen_of_nodup_theClosedSix_of_disjoint {X : Type u_1} [TopologicalSpace X] {s : Set X} (nodup : (theClosedSix s).Nodup) (disj : Disjoint (theClosedSix s) (theOpenSix s)) : (theFourteen s).Nodup

theFourteen s contains no duplicates if and only if theClosedSix s has none, and theClosedSix s is disjoint from theOpenSix s.

def Topology.ClosureCompl.fourteenSet : Set ℝ

A set in ℝ from which the maximum of 14 distinct sets can be obtained.

Equations

• Topology.ClosureCompl.fourteenSet = Set.Ioo 0 1 ∪ Set.Ioo 1 2 ∪ {3} ∪ Set.Icc 4 5 ∩ Set.range Rat.cast

Let the fourteenSet be s: (0,1) ∪ (1,2) ∪ {3} ∪ ([4,5] ∩ ℚ) Then the following sets can be obtained via the closure and complement operations:

• cs = (-∞,0] ∪ {1} ∪ [2,3) ∪ (3,4) ∪ ([4,5] \ ℚ) ∪ (5,∞)
• kcs = (-∞,0] ∪ {1} ∪ [2,∞)
• ckcs = (0,1) ∪ (1,2)
• kckcs = [0,2]
• ckckcs = (-∞,0) ∪ (2,∞)
• kckckcs = (-∞,0] ∪ [2,∞)
• ckckckcs = (0,2)
• ks = [0,2] ∪ {3} ∪ [4,5]
• cks = (-∞,0) ∪ (2,3) ∪ (3,4) ∪ (5,∞)
• kcks = (-∞,0] ∪ [2,4] ∪ [5,∞)
• ckcks = (0,2) ∪ (4,5)
• kckcks = [0,2] ∪ [4,5]
• ckckcks = (-∞,0) ∪ (2,4) ∪ (5,∞)

We can see that the sets are pairwise distinct, so we have 14 distinct sets.

theorem Topology.ClosureCompl.k_Icc_4_5_inter_rat : closure (Set.Icc 4 5 ∩ Set.range Rat.cast) = Set.Icc 4 5

theorem Topology.ClosureCompl.i_fourteenSet : interior fourteenSet = Set.Ioo 0 1 ∪ Set.Ioo 1 2

theorem Topology.ClosureCompl.k_fourteenSet : closure fourteenSet = Set.Icc 0 2 ∪ {3} ∪ Set.Icc 4 5

theorem Topology.ClosureCompl.kc_fourteenSet : closure fourteenSetᶜ = (Set.Ioo 0 1 ∪ Set.Ioo 1 2)ᶜ

theorem Topology.ClosureCompl.kck_fourteenSet : closure (closure fourteenSet)ᶜ = (Set.Ioo 0 2 ∪ Set.Ioo 4 5)ᶜ

theorem Topology.ClosureCompl.kckc_fourteenSet : closure (closure fourteenSetᶜ)ᶜ = Set.Icc 0 2

theorem Topology.ClosureCompl.kckck_fourteenSet : closure (closure (closure fourteenSet)ᶜ)ᶜ = Set.Icc 0 2 ∪ Set.Icc 4 5

theorem Topology.ClosureCompl.kckckc_fourteenSet : closure (closure (closure fourteenSetᶜ)ᶜ)ᶜ = (Set.Ioo 0 2)ᶜ

theorem Topology.ClosureCompl.nodup_theClosedSix_fourteenSet : (theClosedSix fourteenSet).Nodup

theClosedSix applied to the specific fourteenSet generates no duplicates.

theorem Topology.ClosureCompl.nonempty_of_mem_theClosedSix_fourteenSet {s : Set ℝ} (h : s ∈ theClosedSix fourteenSet) : s.Nonempty

No set from theClosedSix fourteenSet is empty.

theorem Topology.ClosureCompl.not_eq_univ_of_mem_theClosedSix_fourteenSet {s : Set ℝ} (h : s ∈ theClosedSix fourteenSet) : s ≠ Set.univ

No set from theClosedSix fourteenSet is the universal set.

theorem Topology.ClosureCompl.nodup_theFourteen_fourteenSet : (theFourteen fourteenSet).Nodup

The fourteen different operations applied to the fourteenSet generate no duplicates.

theorem Topology.ClosureCompl.ncard_isObtainable_fourteenSet : {t : Set ℝ | IsObtainable fourteenSet t}.ncard = 14

The number of distinct sets obtainable from fourteenSet is exactly 14.