zero_mem_cantorSet

Mathlib.Topology.Instances.CantorSet

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

English

0 ∈ cantorSet.

Русский

0 принадлежит Канторову множеству.

LaTeX

$$$0 \in \text{cantorSet}$$$

Lean4

theorem zero_mem_cantorSet : 0 ∈ cantorSet := by simp [cantorSet, zero_mem_preCantorSet]

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

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

Разделы

Аффилиация

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