zero_mem_preCantorSet — Mathlib

English

The family {preCantorSet(n)} is decreasing in n: if m ≤ n then preCantorSet(n) ⊆ preCantorSet(m).

Русский

Множество {preCantorSet(n)} убывает при увеличении n: если m ≤ n, то preCantorSet(n) ⊆ preCantorSet(m).

LaTeX

$$∀ m ≤ n, preCantorSet(n) ⊆ preCantorSet(m).$$

Lean4

theorem zero_mem_preCantorSet (n : ℕ) : 0 ∈ preCantorSet n := by
  induction n with
  | zero => simp [preCantorSet]
  | succ n ih => exact Or.inl ⟨0, ih, by simp only [zero_div]⟩

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