hasBasis_nhds_zero' — Mathlib

English

Another unmarshaled form of the zero-neighborhood basis: (nhds 0).HasBasis (γ ≠ 0) ({x | v x < γ}).

Русский

Ещё одно представление базиса нулевой окрестности: (nhds 0).HasBasis (γ ≠ 0) ({x | v x < γ}).

LaTeX

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

Lean4

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

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