nhdsWithin_hasBasis — Mathlib

English

A basis for nhdsWithin a t is given by intersections of a basis with t.

Русский

Базис для nhdsWithin a t задаётся пересечениями базисa с t.

LaTeX

$$$(nhdsWithin a t).HasBasis (fun u => a ∈ u ∧ IsOpen u) (\,u \mapsto u \cap t\,)$$$

Lean4

theorem nhdsWithin_hasBasis {ι : Sort*} {p : ι → Prop} {s : ι → Set α} {a : α} (h : (𝓝 a).HasBasis p s) (t : Set α) :
    (𝓝[t] a).HasBasis p fun i => s i ∩ t :=
  h.inf_principal t

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