English
Let preCantorSet(n) be defined recursively by: preCantorSet(0) = [0,1], and preCantorSet(n+1) = (1/3) preCantorSet(n) ∪ { (2+x)/3 : x ∈ preCantorSet(n) }. This describes the order-n pre-Cantor set obtained by repeatedly removing the middle third of each interval.
Русский
Пусть preCantorSet(n) задаётся рекурсивно: preCantorSet(0) = [0,1], и preCantorSet(n+1) = (1/3)·preCantorSet(n) ∪ { (2+x)/3 : x ∈ preCantorSet(n) }. Это так называемое порядковое n предканторово множество, получаемое последовательным вырезанием середины каждого интервала.
LaTeX
$$$\text{preCantorSet}(0) = [0,1],\quad \text{preCantorSet}(n+1) = \frac{1}{3}\,\text{preCantorSet}(n) \cup \left\{ \frac{2+x}{3} : x \in \text{preCantorSet}(n) \right\}. $$$
Lean4
/-- 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`.
-/
def preCantorSet : ℕ → Set ℝ
| 0 => Set.Icc 0 1
| n + 1 => (· / 3) '' preCantorSet n ∪ (fun x ↦ (2 + x) / 3) '' preCantorSet n
