hasBasis_nhds' — Mathlib

English

A variant of the neighborhood basis at x using the nonzero γ parametrization: (nhds x).HasBasis (γ ≠ 0) ({ z - x | v(z) < γ }).

Русский

Вариант базиса окрестностей в точке x с использованием ненулевых γ: (nhds x).HasBasis (γ ≠ 0) ({ z − x | v(z) < γ }).

LaTeX

$$(nhds x).HasBasis (γ ≠ 0) ({ z | v(z - x) < γ })$$

Lean4

/-- A variant of `hasBasis_nhds` where `· ≠ 0` is unbundled. -/
theorem hasBasis_nhds' (x : R) : (𝓝 x).HasBasis (· ≠ 0) ({y | v (y - x) < ·}) :=
  (hasBasis_nhds x).to_hasBasis (fun γ _ ↦ ⟨γ, by simp⟩) fun γ hγ ↦ ⟨.mk0 γ hγ, by simp⟩

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