hasBasis_nhds_of_ne_top — Mathlib

English

There is a basis of neighborhoods of x ≠ ∞ given by intervals Icc(x−ε, x+ε) with ε>0.

Русский

Существует базис окрестностей точки x ≠ ∞, состоящий из интервалов Icc(x−ε, x+ε) при ε>0.

LaTeX

$$HasBasis_nhds_of_ne_top (xt : x ≠ ∞) : (nhds x).HasBasis (0 < ·) (ε ↦ Icc(x-ε, x+ε))$$

Lean4

theorem hasBasis_nhds_of_ne_top (xt : x ≠ ∞) : (𝓝 x).HasBasis (0 < ·) (fun ε => Icc (x - ε) (x + ε)) := by
  simpa only [pos_iff_ne_zero] using hasBasis_nhds_of_ne_top' xt

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