|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Jan Förster, Leon Müller, Luis Sand, and Junyan Xu. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Jan Förster, Leon Müller, Luis Sand, Junyan Xu |
| 5 | +-/ |
| 6 | +import Mathlib.Topology.Instances.Irrational |
| 7 | +import Mathlib.Topology.Instances.Real.Lemmas |
| 8 | +import Archive.Kuratowski |
| 9 | + |
| 10 | +/-! |
| 11 | +# Kuratowski's closure-complement theorem is sharp |
| 12 | +
|
| 13 | +Kuratowski's closure-complement theorem says that if one repeatedly applies the closure and |
| 14 | +complement operators to a set in a topological space, at most 14 distinct sets can be obtained. |
| 15 | +
|
| 16 | +This file gives an example of a so-called "14-set" in ℝ, from which exactly 14 distinct sets |
| 17 | +can be obtained. |
| 18 | +
|
| 19 | +Our strategy is to show there is no duplication within the fourteen sets obtained from this set |
| 20 | +`s`: the fourteen sets can be decomposed into six closed sets, six open sets that are the |
| 21 | +complements of the closed sets, and `s` and `sᶜ` which are neither closed nor open. |
| 22 | +This reduces `14*13/2 = 91` inequalities to check down to `6*5/2 = 15` inequalities. |
| 23 | +We'll further show that the 15 inequalities follow from a subset of 6 by algebra. |
| 24 | +
|
| 25 | +There are charaterizations and criteria for a set to be a 14-set in the paper |
| 26 | +"Characterization of Kuratowski 14-Sets" by Eric Langford which we do not formalize. |
| 27 | +
|
| 28 | +## Main definitions |
| 29 | +
|
| 30 | +* `Topology.ClosureCompl.fourteenSet`: an explicit example of a 14-set in ℝ. |
| 31 | +* `Topology.ClosureCompl.theClosedSix`: the six open sets obtainable from a given set. |
| 32 | +* `Topology.ClosureCompl.theOpenSix`: the six open sets obtainable from a given set. |
| 33 | +* `Topology.ClosureCompl.TheSixIneq`: six inequalities that suffice to deduce |
| 34 | + that the six closed sets obtained from a given set contain no duplicates. |
| 35 | +
|
| 36 | +## Main results |
| 37 | +
|
| 38 | +* `Topology.ClosureCompl.nodup_theFourteen_fourteenSet`: |
| 39 | + the application of all 14 operations on the defined `fourteenSet` in ℝ gives no duplicates. |
| 40 | +
|
| 41 | +* `Topology.ClosureCompl.ncard_isObtainable_fourteenSet`: |
| 42 | + for the defined `fourteenSet` in ℝ, there are exactly 14 distinct sets that can be obtained from |
| 43 | + `fourteenSet` using the closure and complement operations. |
| 44 | +-/ |
| 45 | + |
| 46 | +namespace Topology.ClosureCompl |
| 47 | + |
| 48 | +variable {X : Type*} [TopologicalSpace X] {s t : Set X} |
| 49 | + |
| 50 | + |
| 51 | +/-- The six closed sets obtained from a given set `s` are given by applying |
| 52 | +`k, kc, kck, kckc, kckck, kckckc` to `s`. -/ |
| 53 | +def theClosedSix (s : Set X) : Multiset (Set X) := |
| 54 | + {k s, k sᶜ, k (k s)ᶜ, k (k sᶜ)ᶜ, k (k (k s)ᶜ)ᶜ, k (k (k sᶜ)ᶜ)ᶜ} |
| 55 | + |
| 56 | +/-- The complements of the six closed sets. -/ |
| 57 | +def theOpenSix (s : Set X) : Multiset (Set X) := |
| 58 | + (theClosedSix s).map compl |
| 59 | + |
| 60 | +/- By applying the identity and complement operations to the six closed sets, we obtain |
| 61 | +precisely the six closed sets plus the six open sets. -/ |
| 62 | +theorem sum_map_theClosedSix_add_compl (s : Set X) : |
| 63 | + ((theClosedSix s).map fun t ↦ {t} + {tᶜ}).sum = theClosedSix s + theOpenSix s := |
| 64 | + Multiset.sum_map_add |
| 65 | + |
| 66 | +/-- `theFourteen s` can be splitted into 3 subsets. -/ |
| 67 | +theorem theFourteen_eq_pair_add_theClosedSix_add_theOpenSix (s : Set X) : |
| 68 | + theFourteen s = {s, sᶜ} + theClosedSix s + theOpenSix s := by |
| 69 | + rw [add_assoc, ← sum_map_theClosedSix_add_compl]; rfl |
| 70 | + |
| 71 | +/-- Every set in `theClosedSix s` is closed (because the last operation is closure). -/ |
| 72 | +theorem isClosed_of_mem_theClosedSix (h : t ∈ theClosedSix s) : IsClosed t := by |
| 73 | + repeat obtain _ | ⟨_, h⟩ := h; rotate_left |
| 74 | + all_goals exact isClosed_closure |
| 75 | + |
| 76 | +/-- Every set in `theOpenSix s` is open. -/ |
| 77 | +theorem isOpen_of_mem_theOpenSix (h : t ∈ theOpenSix s) : IsOpen t := by |
| 78 | + obtain ⟨t, ht, rfl⟩ := Multiset.mem_map.mp h |
| 79 | + exact (isClosed_of_mem_theClosedSix ht).isOpen_compl |
| 80 | + |
| 81 | +theorem mem_theOpenSix_iff : t ∈ theOpenSix s ↔ tᶜ ∈ theClosedSix s := by |
| 82 | + conv_lhs => rw [theOpenSix, ← compl_compl t, Multiset.mem_map_of_injective compl_injective] |
| 83 | + |
| 84 | +/-- Six inequalities that suffice to deduce the six closed sets obtained from a given set |
| 85 | +contain no duplicates. -/ |
| 86 | +def TheSixIneq (s : Set X) : Prop := |
| 87 | + k (k (k sᶜ)ᶜ)ᶜ ≠ k (k (k s)ᶜ)ᶜ |
| 88 | + ∧ k (k (k sᶜ)ᶜ)ᶜ ≠ k (k sᶜ)ᶜ |
| 89 | + ∧ k (k (k sᶜ)ᶜ)ᶜ ≠ k (k s)ᶜ |
| 90 | + ∧ k (k (k sᶜ)ᶜ)ᶜ ≠ k sᶜ |
| 91 | + ∧ k (k (k s)ᶜ)ᶜ ≠ k (k s)ᶜ |
| 92 | + ∧ k (k (k s)ᶜ)ᶜ ≠ k s |
| 93 | + |
| 94 | +open Multiset in |
| 95 | +/-- `theClosedSix` applied to an arbitrary set `s` results in no duplicates iff `TheSixIneq` |
| 96 | +is true for `s`. -/ |
| 97 | +theorem nodup_theClosedSix_theFourteen_iff : (theClosedSix s).Nodup ↔ TheSixIneq s := by |
| 98 | + rw [TheSixIneq, theClosedSix] |
| 99 | + simp only [insert_eq_cons, nodup_cons, mem_cons, mem_singleton, |
| 100 | + not_or, nodup_singleton, and_true, ← ne_eq, and_assoc] |
| 101 | + -- The goal becomes 6 inequalities ↔ 15 inequalities. |
| 102 | + constructor -- Show both implications. |
| 103 | + · -- One implication is almost trivial as the six inequalities are among the fifteen. |
| 104 | + tauto |
| 105 | + · intro h -- Introduce `TheSixIneq` as an assumption. |
| 106 | + repeat obtain ⟨_, h⟩ := h -- Split the hypothesis into six different inequalities. |
| 107 | + repeat refine .symm (.intro ?_ ?_) -- Split the goal into 15 inequalities. |
| 108 | + any_goals |
| 109 | + rw [ne_comm] |
| 110 | + try assumption |
| 111 | + -- Solve trivial goals (the six inequalities contained in `TheSixIneq`). |
| 112 | + any_goals |
| 113 | + /- Now eight other goals can be solved by simplifying |
| 114 | + and then using one of the six given inequalities. -/ |
| 115 | + apply mt (congr_arg (k ·ᶜ)) |
| 116 | + first |
| 117 | + | try repeat rw [kckckck_eq_kck, eq_comm] |
| 118 | + assumption |
| 119 | + | apply mt (congr_arg (k ·ᶜ)) |
| 120 | + try repeat rw [kckckck_eq_kck, eq_comm] |
| 121 | + assumption |
| 122 | + -- One last goal (`k (k (k sᶜ)ᶜ)ᶜ ≠ k s`) needs some other simplifying steps: |
| 123 | + · apply mt (congr_arg fun s ↦ k (k sᶜ)ᶜ) |
| 124 | + rw [kckckck_eq_kck] |
| 125 | + assumption |
| 126 | + |
| 127 | +open Multiset in |
| 128 | +/-- `theFourteen s` contains no duplicates if and only if `theClosedSix s` has none, |
| 129 | +and `theClosedSix s` is disjoint from `theOpenSix s`. -/ |
| 130 | +theorem nodup_theFourteen_of_nodup_theClosedSix_of_disjoint |
| 131 | + (nodup : (theClosedSix s).Nodup) (disj : Disjoint (theClosedSix s) (theOpenSix s)) : |
| 132 | + (theFourteen s).Nodup := by |
| 133 | + rw [theFourteen_eq_pair_add_theClosedSix_add_theOpenSix, add_assoc, nodup_add, nodup_add] |
| 134 | + refine ⟨?_, ⟨nodup, nodup.map compl_injective, disj⟩, ?_⟩ |
| 135 | + -- The two goals now are {s, sᶜ}.Nodup and Disjoint {s, sᶜ} (theClosedSix s + theOpenSix s). |
| 136 | + · -- The first follows from nontriviality of the topological space. |
| 137 | + have : Nontrivial (Set X) := ⟨_, _, (List.pairwise_cons.mp nodup).1 _ (.head _)⟩ |
| 138 | + simp |
| 139 | + have hs : ¬ IsClosed s := fun h ↦ by simp [theClosedSix] at nodup |
| 140 | + have hsc : ¬ IsClosed sᶜ := fun h ↦ by simp [theClosedSix] at nodup |
| 141 | + -- Show `s ∉ theClosedSix s ∧ sᶜ ∉ theClosedSix s` and `s ∉ theOpenSix s ∧ sᶜ ∉ theOpenSix s`. |
| 142 | + simp only [insert_eq_cons, disjoint_add_right, disjoint_cons_left, singleton_disjoint, |
| 143 | + mem_theOpenSix_iff, compl_compl, and_comm, and_self] |
| 144 | + exact ⟨(hs <| isClosed_of_mem_theClosedSix ·), (hsc <| isClosed_of_mem_theClosedSix ·)⟩ |
| 145 | + |
| 146 | +open Set |
| 147 | + |
| 148 | +/-- A set in `ℝ` from which the maximum of 14 distinct sets can be obtained. -/ |
| 149 | +def fourteenSet : Set ℝ := Ioo 0 1 ∪ Ioo 1 2 ∪ {3} ∪ (Icc 4 5 ∩ range Rat.cast) |
| 150 | + |
| 151 | +/-! |
| 152 | +Let the fourteenSet be s: `(0,1) ∪ (1,2) ∪ {3} ∪ ([4,5] ∩ ℚ)` |
| 153 | +Then the following sets can be obtained via the closure and complement operations: |
| 154 | +* `cs = (-∞,0] ∪ {1} ∪ [2,3) ∪ (3,4) ∪ ([4,5] \ ℚ) ∪ (5,∞)` |
| 155 | +* `kcs = (-∞,0] ∪ {1} ∪ [2,∞)` |
| 156 | +* `ckcs = (0,1) ∪ (1,2)` |
| 157 | +* `kckcs = [0,2]` |
| 158 | +* `ckckcs = (-∞,0) ∪ (2,∞)` |
| 159 | +* `kckckcs = (-∞,0] ∪ [2,∞)` |
| 160 | +* `ckckckcs = (0,2)` |
| 161 | +* `ks = [0,2] ∪ {3} ∪ [4,5]` |
| 162 | +* `cks = (-∞,0) ∪ (2,3) ∪ (3,4) ∪ (5,∞)` |
| 163 | +* `kcks = (-∞,0] ∪ [2,4] ∪ [5,∞)` |
| 164 | +* `ckcks = (0,2) ∪ (4,5)` |
| 165 | +* `kckcks = [0,2] ∪ [4,5]` |
| 166 | +* `ckckcks = (-∞,0) ∪ (2,4) ∪ (5,∞)` |
| 167 | +
|
| 168 | +We can see that the sets are pairwise distinct, so we have 14 distinct sets. |
| 169 | +-/ |
| 170 | + |
| 171 | +theorem k_Icc_4_5_inter_rat : k (Icc (4 : ℝ) 5 ∩ range Rat.cast) = Icc 4 5 := |
| 172 | + (closure_ordConnected_inter_rat ordConnected_Icc ⟨4, by norm_num, 5, by norm_num⟩).trans |
| 173 | + isClosed_Icc.closure_eq |
| 174 | + |
| 175 | +theorem i_fourteenSet : i fourteenSet = Ioo 0 1 ∪ Ioo 1 2 := by |
| 176 | + have := interior_eq_empty_iff_dense_compl.mpr dense_irrational |
| 177 | + rw [fourteenSet, interior_union_of_disjoint_closure, interior_union_of_disjoint_closure] |
| 178 | + · simp [(isOpen_Ioo.union isOpen_Ioo).interior_eq, this] |
| 179 | + all_goals norm_num [-union_singleton, k_Icc_4_5_inter_rat, |
| 180 | + disjoint_iff_inter_eq_empty, union_inter_distrib_right, Icc_inter_Icc] |
| 181 | + |
| 182 | +theorem k_fourteenSet : k fourteenSet = Icc 0 2 ∪ {3} ∪ Icc 4 5 := by |
| 183 | + simp_rw [fourteenSet, closure_union] |
| 184 | + rw [closure_Ioo, closure_Ioo, k_Icc_4_5_inter_rat, Icc_union_Icc'] |
| 185 | + all_goals norm_num |
| 186 | + |
| 187 | +theorem kc_fourteenSet : k fourteenSetᶜ = (Ioo 0 1 ∪ Ioo 1 2)ᶜ := by |
| 188 | + rw [closure_compl, compl_inj_iff, i_fourteenSet] |
| 189 | + |
| 190 | +theorem kck_fourteenSet : k (k fourteenSet)ᶜ = (Ioo 0 2 ∪ Ioo 4 5)ᶜ := by |
| 191 | + rw [closure_compl, k_fourteenSet, |
| 192 | + interior_union_of_disjoint_closure, interior_union_of_disjoint_closure] |
| 193 | + all_goals norm_num |
| 194 | + [-union_singleton, disjoint_iff_inter_eq_empty, union_inter_distrib_right, Icc_inter_Icc] |
| 195 | + |
| 196 | +theorem kckc_fourteenSet : k (k fourteenSetᶜ)ᶜ = Icc 0 2 := by |
| 197 | + rw [kc_fourteenSet, compl_compl, closure_union, closure_Ioo, closure_Ioo] |
| 198 | + all_goals norm_num |
| 199 | + |
| 200 | +theorem kckck_fourteenSet : k (k (k fourteenSet)ᶜ)ᶜ = Icc 0 2 ∪ Icc 4 5 := by |
| 201 | + rw [kck_fourteenSet, compl_compl, closure_union, closure_Ioo, closure_Ioo] |
| 202 | + all_goals norm_num |
| 203 | + |
| 204 | +theorem kckckc_fourteenSet : k (k (k fourteenSetᶜ)ᶜ)ᶜ = (Ioo 0 2)ᶜ := by |
| 205 | + rw [kckc_fourteenSet, closure_compl, interior_Icc] |
| 206 | + |
| 207 | +/-- `theClosedSix` applied to the specific `fourteenSet` generates no duplicates. -/ |
| 208 | +theorem nodup_theClosedSix_fourteenSet : (theClosedSix fourteenSet).Nodup := by |
| 209 | + rw [nodup_theClosedSix_theFourteen_iff, TheSixIneq, kckckc_fourteenSet, kckck_fourteenSet, |
| 210 | + kckc_fourteenSet, kck_fourteenSet, kc_fourteenSet, k_fourteenSet] |
| 211 | + refine ⟨(ne_of_mem_of_not_mem' (a := 1) ?_ ?_).symm, |
| 212 | + (ne_of_mem_of_not_mem' (a := 1) ?_ ?_).symm, |
| 213 | + ne_of_mem_of_not_mem' (a := 4.5) ?_ ?_, |
| 214 | + (ne_of_mem_of_not_mem' (a := 1) ?_ ?_).symm, |
| 215 | + ne_of_mem_of_not_mem' (a := 1) ?_ ?_, |
| 216 | + (ne_of_mem_of_not_mem' (a := 3) ?_ ?_).symm⟩ |
| 217 | + all_goals norm_num |
| 218 | + |
| 219 | +/-- No set from `theClosedSix fourteenSet` is empty. -/ |
| 220 | +theorem nonempty_of_mem_theClosedSix_fourteenSet {s} |
| 221 | + (h : s ∈ theClosedSix fourteenSet) : s.Nonempty := by |
| 222 | + rw [theClosedSix, kckckc_fourteenSet, kckck_fourteenSet, |
| 223 | + kckc_fourteenSet, kck_fourteenSet, kc_fourteenSet, k_fourteenSet] at h |
| 224 | + repeat obtain _ | ⟨_, h⟩ := h; rotate_left |
| 225 | + all_goals use 2; norm_num |
| 226 | + |
| 227 | +/-- No set from `theClosedSix fourteenSet` is the universal set. -/ |
| 228 | +theorem not_eq_univ_of_mem_theClosedSix_fourteenSet {s} |
| 229 | + (h : s ∈ theClosedSix fourteenSet) : s ≠ univ := by |
| 230 | + rw [theClosedSix, kckckc_fourteenSet, kckck_fourteenSet, |
| 231 | + kckc_fourteenSet, kck_fourteenSet, kc_fourteenSet, k_fourteenSet] at h |
| 232 | + rw [Ne, eq_univ_iff_forall] |
| 233 | + push_neg |
| 234 | + repeat obtain _ | ⟨_, h⟩ := h; rotate_left |
| 235 | + · use 1/2; norm_num |
| 236 | + · use 1/2; norm_num |
| 237 | + · use 6; norm_num |
| 238 | + · use 6; norm_num |
| 239 | + · use 1/2; norm_num |
| 240 | + · use 6; norm_num |
| 241 | + |
| 242 | +/-- The fourteen different operations applied to the `fourteenSet` generate no duplicates. -/ |
| 243 | +theorem nodup_theFourteen_fourteenSet : (theFourteen fourteenSet).Nodup := |
| 244 | + nodup_theFourteen_of_nodup_theClosedSix_of_disjoint nodup_theClosedSix_fourteenSet <| |
| 245 | + Multiset.disjoint_iff_ne.mpr <| by |
| 246 | + rintro s hc _ ho rfl |
| 247 | + exact not_eq_univ_of_mem_theClosedSix_fourteenSet hc <| IsClopen.eq_univ |
| 248 | + ⟨isClosed_of_mem_theClosedSix hc, isOpen_of_mem_theOpenSix ho⟩ |
| 249 | + (nonempty_of_mem_theClosedSix_fourteenSet hc) |
| 250 | + |
| 251 | +/-- The number of distinct sets obtainable from `fourteenSet` is exactly 14. -/ |
| 252 | +theorem ncard_isObtainable_fourteenSet : {t | IsObtainable fourteenSet t}.ncard = 14 := by |
| 253 | + classical rw [← card_theFourteen fourteenSet, ← Multiset.toFinset_card_of_nodup |
| 254 | + nodup_theFourteen_fourteenSet, ← Set.ncard_coe_finset] |
| 255 | + congr; ext; simp [mem_theFourteen_iff_isObtainable] |
| 256 | + |
| 257 | +end Topology.ClosureCompl |
0 commit comments