mem_nhds_toTopsp — Mathlib

English

A neighborhood basis for nhds in the topological space given by F is described by subsets generated from the realizations F.

Русский

Основание окрестности nhds в топологическом пространстве, заданном F, описывается через подмножества, порождаемые реализациями F.

LaTeX

$$$s \\in nhds\\ a \\iff \\exists b, a \\in F.b ∧ F.b \\subseteq s$$$

Lean4

@[simp]
theorem mem_nhds_toTopsp (F : Ctop α σ) {s : Set α} {a : α} : s ∈ @nhds _ F.toTopsp a ↔ ∃ b, a ∈ F b ∧ F b ⊆ s :=
  (@TopologicalSpace.IsTopologicalBasis.mem_nhds_iff _ F.toTopsp _ _ _ F.toTopsp_isTopologicalBasis).trans <|
    ⟨fun ⟨_, ⟨x, rfl⟩, h⟩ ↦ ⟨x, h⟩, fun ⟨x, h⟩ ↦ ⟨_, ⟨x, rfl⟩, h⟩⟩

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