preCantorSet_succ — Mathlib

English

For any n, preCantorSet(n+1) is the union of the images of preCantorSet(n) under the maps x ↦ x/3 and x ↦ (2+x)/3.

Русский

Для любого n предканторово множество следующего шага равно объединению образов предканторового множества n под отображениями x ↦ x/3 и x ↦ (2+x)/3.

LaTeX

$$$\text{preCantorSet}(n+1) = \frac{1}{3} \text{preCantorSet}(n) \cup \left\{ \frac{2+x}{3} : x \in \text{preCantorSet}(n) \right\}. $$$

Lean4

@[simp]
theorem preCantorSet_succ (n : ℕ) :
    preCantorSet (n + 1) = (· / 3) '' preCantorSet n ∪ (fun x ↦ (2 + x) / 3) '' preCantorSet n :=
  rfl

Похожие утверждения