English
For any r ∈ ValueGroupWithZero R with r ≠ 0, the ball { x ∈ R : v(x) < r } is open.
Русский
Для любого r ∈ ValueGroupWithZero R с r ≠ 0 шар { x ∈ R : v(x) < r } открыт.
LaTeX
$$$\\forall r\\in ValueGroupWithZero(R),\\ r \\neq 0 \\implies \\operatorname{IsOpen}\\{x \\in R \\mid v(x) < r\\}$$$
Lean4
theorem isOpen_ball (r : ValueGroupWithZero R) : IsOpen {x | v x < r} :=
by
rw [isOpen_iff_mem_nhds]
rcases eq_or_ne r 0 with rfl | hr
· simp
· intro x hx
rw [mem_nhds_iff']
simp only [setOf_subset_setOf]
exact ⟨Units.mk0 _ hr, fun y hy => (sub_add_cancel y x).symm ▸ ((v).map_add _ x).trans_lt (max_lt hy hx)⟩