isClosed_preCantorSet — Mathlib

English

For every n, preCantorSet(n) is closed.

Русский

Для каждого n множество preCantorSet(n) является замкнутым.

LaTeX

$$$\forall n,\ IsClosed(\text{preCantorSet}(n)).$$$

Lean4

/-- The preCantor sets are closed. -/
theorem isClosed_preCantorSet (n : ℕ) : IsClosed (preCantorSet n) :=
  by
  let f := Homeomorph.mulLeft₀ (1 / 3 : ℝ) (by simp)
  let g := (Homeomorph.addLeft (2 : ℝ)).trans f
  induction n with
  | zero => exact isClosed_Icc
  | succ n ih =>
    refine IsClosed.union ?_ ?_
    · simpa [f, div_eq_inv_mul] using f.isClosedEmbedding.isClosed_iff_image_isClosed.mp ih
    · simpa [g, f, div_eq_inv_mul] using g.isClosedEmbedding.isClosed_iff_image_isClosed.mp ih

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