nhdsWithin_basis_ball — Mathlib

English

The restricted neighborhood filter at x within s has a basis consisting of ball intersections with s for all ε>0.

Русский

Ограниченный фильтр окрестностей x внутри s имеет базис, состоящий из пересечений шаров с s для всех ε>0.

LaTeX

$$(nhdsWithin x s) has basis { B(x, ε) ∩ s : ε > 0 }.$$

Lean4

theorem nhdsWithin_basis_ball {s : Set α} : (𝓝[s] x).HasBasis (fun ε : ℝ => 0 < ε) fun ε => ball x ε ∩ s :=
  nhdsWithin_hasBasis nhds_basis_ball s

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