English
The uniformity basis is given by γ ∈ Γ₀ˣ with sets { (p,q) ∈ R×R : v(q−p) < γ }.
Русский
Базис униформности задаётся γ ∈ Γ₀ˣ множествами { (p,q) : R×R : v(q−p) < γ }.
LaTeX
$$$\{(p,q) \in R\times R : v(q-p) < γ\}$$$
Lean4
/-- An open ball centred at the origin in a valued ring is open. -/
theorem isOpen_ball (r : Γ₀) : IsOpen (X := R) {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]
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)⟩