isClosed_closedBall — Mathlib

English

The closed ball { x : R : v(x) ≤ r } is closed (for any r).

Русский

Замкованный шар { x : R : v(x) ≤ r } замкнут.

LaTeX

$$$\{x : R : v(x) \le r\}$ закрыт$$

Lean4

/-- A closed ball centred at the origin in a valued ring is closed. -/
theorem isClosed_closedBall (r : Γ₀) : IsClosed (X := R) {x | v x ≤ r} :=
  by
  rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
  intro x hx
  rw [mem_nhds]
  have hx' : v x ≠ 0 := ne_of_gt <| lt_of_le_of_lt zero_le' <| lt_of_not_ge hx
  exact
    ⟨Units.mk0 _ hx', fun y hy hy' =>
      ne_of_lt hy <| map_sub_swap v x y ▸ (Valuation.map_sub_eq_of_lt_left _ <| lt_of_le_of_lt hy' (lt_of_not_ge hx))⟩

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