nhdsWithin_basis_eball — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem nhdsWithin_basis_eball : (𝓝[s] x).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) fun ε => ball x ε ∩ s :=
  nhdsWithin_hasBasis nhds_basis_eball s

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