isClosed_sphere — Mathlib

English

For any r ∈ Γ₀, the sphere { x ∈ R : v(x) = r } is a closed subset of R.

Русский

Для любого r ∈ Γ₀ сфера { x ∈ R : v(x) = r } является замкнутым подмножеством R.

LaTeX

$$$\\forall r ∈ Γ_0,\\ IsClosed\\left(\\{x \\in R \\mid v(x) = r\\}\\right)$$$

Lean4

/-- A sphere centred at the origin in a valued ring is closed. -/
theorem isClosed_sphere (r : Γ₀) : IsClosed (X := R) {x | v x = r} :=
  by
  rcases eq_or_ne r 0 with rfl | hr
  · simpa using isClosed_closedBall R 0
  exact isClopen_sphere _ hr |>.isClosed

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