nhdsWithin_basis_closed_eball — Mathlib

English

The nhdsWithin structure has a basis given by closed balls intersected with a set.

Русский

Структура nhdsWithin имеет базис, задаваемый замкнутыми шарами пересеченными с данным множеством.

LaTeX

$$$ (\\mathrm{nhdsWithin}\\, x\\, s) \\text{HasBasis} (\\lambda \\varepsilon. 0 < \\varepsilon) (\\lambda \\varepsilon. \\mathrm{closedBall}(x,\\varepsilon) \\cap s) $$$

Lean4

theorem nhdsWithin_basis_closed_eball : (𝓝[s] x).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) fun ε => closedBall x ε ∩ s :=
  nhdsWithin_hasBasis nhds_basis_closed_eball s

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