isClosed_ball — Mathlib

English

For any r, the closed ball { x ∈ R : v(x) ≤ r } is closed.

Русский

Для любого r замкованный шар { x ∈ R : v(x) ≤ r } замкнуто.

LaTeX

$$$\\forall r,\\ IsClosed\\left(\\{x \\in R \\mid v(x) \\le r\\}\\right)$$$

Lean4

theorem isClosed_ball (r : ValueGroupWithZero R) : IsClosed {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 _)

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