isClosed_closedBall — Mathlib

English

The ball { x : v(x) < r } is open.

Русский

Шар { x : v(x) < r } открыт.

LaTeX

$$IsOpen( {x ∈ R | v(x) < r} )$$

Lean4

theorem isClosed_closedBall (r : ValueGroupWithZero R) : IsClosed {x | v x ≤ r} :=
  by
  rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
  intro x hx
  simp only [mem_compl_iff, mem_setOf_eq, not_le] at hx
  rw [mem_nhds_iff']
  have hx' : v x ≠ 0 := ne_of_gt <| lt_of_le_of_lt zero_le' <| hx
  exact
    ⟨Units.mk0 _ hx', fun y hy hy' =>
      ne_of_lt hy <| Valuation.map_sub_swap v x y ▸ (Valuation.map_sub_eq_of_lt_left _ <| lt_of_le_of_lt hy' hx)⟩

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