isOpen_ball — Mathlib

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)⟩

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