quarter_mem_preCantorSet

Mathlib.Topology.Instances.CantorSet

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

English

For every n, 1/4 ∈ preCantorSet n.

Русский

Для каждого n 1/4 принадлежит preCantorSet n.

LaTeX

$$$\forall n,\ 1/4 \in preCantorSet(n).$$$

Lean4

theorem quarter_mem_preCantorSet (n : ℕ) : 1 / 4 ∈ preCantorSet n :=
  (quarters_mem_preCantorSet n).1

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

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

Разделы

Аффилиация

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