Ternary Cantor Set

This file defines the Cantor ternary set and proves a few properties.

Main Definitions

• preCantorSet n: The order n pre-Cantor set, defined inductively as the union of the images under the functions (· / 3) and ((2 + ·) / 3), with preCantorSet 0 := Set.Icc 0 1, i.e. preCantorSet 0 is the unit interval [0,1].
• cantorSet: The ternary Cantor set, defined as the intersection of all pre-Cantor sets.

def preCantorSet : ℕ → Set ℝ

The order n pre-Cantor set, defined starting from [0, 1] and successively removing the middle third of each interval. Formally, the order n + 1 pre-Cantor set is the union of the images under the functions (· / 3) and ((2 + ·) / 3) of preCantorSet n.

Equations

• preCantorSet 0 = Set.Icc 0 1
• preCantorSet n.succ = (fun (x : ℝ) => x / 3) '' preCantorSet n ∪ (fun (x : ℝ) => (2 + x) / 3) '' preCantorSet n

@[simp]

theorem preCantorSet_zero : preCantorSet 0 = Set.Icc 0 1

@[simp]

theorem preCantorSet_succ (n : ℕ) : preCantorSet (n + 1) = (fun (x : ℝ) => x / 3) '' preCantorSet n ∪ (fun (x : ℝ) => (2 + x) / 3) '' preCantorSet n

def cantorSet : Set ℝ

The Cantor set is the subset of the unit interval obtained as the intersection of all pre-Cantor sets. This means that the Cantor set is obtained by iteratively removing the open middle third of each subinterval, starting from the unit interval [0, 1].

Equations

• cantorSet = ⋂ (n : ℕ), preCantorSet n

Simple Properties

theorem quarters_mem_preCantorSet (n : ℕ) : 1 / 4 ∈ preCantorSet n ∧ 3 / 4 ∈ preCantorSet n

theorem quarter_mem_preCantorSet (n : ℕ) : 1 / 4 ∈ preCantorSet n

theorem quarter_mem_cantorSet : 1 / 4 ∈ cantorSet

theorem zero_mem_preCantorSet (n : ℕ) : 0 ∈ preCantorSet n

theorem zero_mem_cantorSet : 0 ∈ cantorSet

theorem preCantorSet_antitone : Antitone preCantorSet

theorem preCantorSet_subset_unitInterval {n : ℕ} : preCantorSet n ⊆ Set.Icc 0 1

theorem cantorSet_subset_unitInterval : cantorSet ⊆ Set.Icc 0 1

The ternary Cantor set is a subset of [0,1].

theorem cantorSet_eq_union_halves : cantorSet = (fun (x : ℝ) => x / 3) '' cantorSet ∪ (fun (x : ℝ) => (2 + x) / 3) '' cantorSet

The ternary Cantor set satisfies the equation C = C / 3 ∪ (2 / 3 + C / 3).

theorem isClosed_preCantorSet (n : ℕ) : IsClosed (preCantorSet n)

The preCantor sets are closed.

theorem isClosed_cantorSet : IsClosed cantorSet

The ternary Cantor set is closed.

theorem isCompact_cantorSet : IsCompact cantorSet

The ternary Cantor set is compact.