cantorSet_subset_unitInterval

Mathlib.Topology.Instances.CantorSet

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

English

The Cantor set is contained in the unit interval: cantorSet ⊆ [0,1].

Русский

Канторово множество содержится в единичном интервале: C ⊆ [0,1].

LaTeX

$$$\text{cantorSet} \subseteq [0,1].$$$

Lean4

/-- The ternary Cantor set is a subset of [0,1]. -/
theorem cantorSet_subset_unitInterval : cantorSet ⊆ Set.Icc 0 1 :=
  Set.iInter_subset _ 0

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

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

Разделы

Аффилиация

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