isClosed_ball — Mathlib

English

For any r, the set { x ∈ R : v(x) < r } is open (when r ≠ 0).

Русский

Для любого r множество { x ∈ R : v(x) < r } является открытым (если r ≠ 0).

LaTeX

$$$\{x \in R : v(x) < r\}$ открыто при $r \neq 0$$$

Lean4

/-- An open ball centred at the origin in a valued ring is closed. -/
theorem isClosed_ball (r : Γ₀) : IsClosed (X := R) {x | v x < r} :=
  by
  rcases eq_or_ne r 0 with rfl | hr
  · simp
  exact AddSubgroup.isClosed_of_isOpen (Valuation.ltAddSubgroup v (Units.mk0 r hr)) (isOpen_ball _ _)

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