preCantorSet_zero

Mathlib.Topology.Instances.CantorSet

URI: https://scilib.ai/kg/mathlib#preCantorSet_zero

English

The 0th pre-Cantor set is the unit interval: preCantorSet(0) = [0,1].

Русский

0-й предканторово множество равно отрезку [0,1].

LaTeX

$$$ \text{preCantorSet}(0) = [0,1]. $$$

Lean4

@[simp]
theorem preCantorSet_zero : preCantorSet 0 = Set.Icc 0 1 :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru