hasBasis_nhds — Mathlib

English

In IsValuativeTopology, the neighborhood basis at any x is generated by the translates of the basic balls { z | v(z − x) < γ }.

Русский

В IsValuativeTopology базис окрестностей в точке x порождается переносами базовых шаров { z | v(z − x) < γ }.

LaTeX

$$(nhds x).HasBasis (True) (γ ↦ {z ∈ R : v(z - x) < γ})$$

Lean4

theorem hasBasis_nhds (x : R) : (𝓝 x).HasBasis (fun _ => True) fun γ : (ValueGroupWithZero R)ˣ => {z | v (z - x) < γ} :=
  by simp [Filter.hasBasis_iff, mem_nhds_iff']

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