nhds_hasBasis — Mathlib

English

The neighborhood filter at a point a has a basis given by the basis sets b ∈ B containing a.

Русский

Окрестная фильтрация в точке a имеет базис, состоящий из базисных элементов b, содержащих a.

LaTeX

$$nhds_hasBasis {b : Set (Set α)} (hb : IsTopologicalBasis b) {a : α} : (𝓝 a).HasBasis (fun t : Set α => t ∈ b ∧ a ∈ t) fun t => t$$

Lean4

theorem nhds_hasBasis {b : Set (Set α)} (hb : IsTopologicalBasis b) {a : α} :
    (𝓝 a).HasBasis (fun t : Set α => t ∈ b ∧ a ∈ t) fun t => t :=
  ⟨fun s => hb.mem_nhds_iff.trans <| by simp only [and_assoc]⟩

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