mem_nhds_zero_iff — Mathlib

English

The neighborhood system at 0 is generated by the sets { x : v(x) < γ } as γ ranges over units in ValueGroupWithZero.

Русский

Система окрестностей в 0 порождается множествами { x : v(x) < γ }, где γ пробегает по единицам ValueGroupWithZero.

LaTeX

$$$\\forall s,\\ s \\in 𝓝(0) \\iff \\exists γ \\in (ValueGroupWithZero R)^{×},\\{x \\mid v(x) < γ\\} \\subseteq s$$$

Lean4

theorem mem_nhds_zero_iff (s : Set R) : s ∈ 𝓝 (0 : R) ↔ ∃ γ : (ValueGroupWithZero R)ˣ, {x | v x < γ} ⊆ s :=
  by
  convert IsValuativeTopology.mem_nhds_iff' (x := (0 : R))
  rw [sub_zero]

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