cantorSet — Mathlib

English

The Cantor set C is the intersection of all order-n pre-Cantor sets: C = ⋂_{n≥0} preCantorSet(n).

Русский

Канторовoо множество C является пересечением всех предканторовых множеств: C = ⋂_{n≥0} preCantorSet(n).

LaTeX

$$$\operatorname{cantorSet} = \bigcap_{n \in \mathbb{N}} \text{preCantorSet}(n).$$$

Lean4

/-- 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]`.
-/
def cantorSet : Set ℝ :=
  ⋂ n, preCantorSet n

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