loc_const — Mathlib

English

For every x with v(x) ≠ 0, the set { y : R | v(y) = v(x) } is a neighborhood of x.

Русский

Для любого x с v(x) ≠ 0 множество { y : R | v(y) = v(x) } является окрестностью точки x.

LaTeX

$$$\{y \in R : v(y) = v(x)\} \in \mathcal{N}(x) \quad\text{if } v(x) \neq 0$$$

Lean4

theorem loc_const {x : R} (h : (v x : Γ₀) ≠ 0) : {y : R | v y = v x} ∈ 𝓝 x :=
  by
  rw [mem_nhds]
  use Units.mk0 _ h
  rw [Units.val_mk0]
  intro y y_in
  exact Valuation.map_eq_of_sub_lt _ y_in

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