isClopen_sphere — Mathlib

English

For r ≠ 0, the sphere { x : v(x) = r } is clopen.

Русский

Для r ≠ 0 сфера { x : v(x) = r } является клипом (открыто и замкнуто).

LaTeX

$$IsClopen( {x ∈ R | v(x) = r} )$$

Lean4

theorem isClopen_sphere {r : ValueGroupWithZero R} (hr : r ≠ 0) : IsClopen {x | v x = r} :=
  by
  have h : {x : R | v x = r} = {x | v x ≤ r} \ {x | v x < r} :=
    by
    ext x
    simp [← le_antisymm_iff]
  rw [h]
  exact IsClopen.diff (isClopen_closedBall hr) (isClopen_ball _)

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