nhds_basis_ball — Mathlib

English

In Euclidean space, the neighborhood filter at x has a basis consisting of open balls centered at x with positive radius.

Русский

В Евклидовом пространстве фильтр окрестностей в точке x имеет базис, состоящий из открытых шаров с центром в x и положительным радиусом.

LaTeX

$$$ (\mathcal{N}(x)).HasBasis(\lambda r: 0 < r)(\mathrm{ball}(x)) $$$

Lean4

theorem nhds_basis_ball {x : E} : (𝓝 x).HasBasis (fun r : ℝ => 0 < r) (ball x) :=
  by
  rw [toEuclidean.toHomeomorph.nhds_eq_comap x]
  exact Metric.nhds_basis_ball.comap _

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