isTopologicalBasis_singletons — Mathlib

English

Let α be a set with the discrete topology. Then the collection of all singleton subsets {x} (x ∈ α) forms a topological basis for α.

Русский

Пусть α является множеством с дискретной топологией. Тогда множество подмножеств вида {x} (x ∈ α) образует базис топологии на α.

LaTeX

$$$\mathrm{IsTopologicalBasis}\bigl(\{\{x\} : x \in \alpha\}\bigr)$$$

Lean4

theorem isTopologicalBasis_singletons (α : Type*) [TopologicalSpace α] [DiscreteTopology α] :
    IsTopologicalBasis {s | ∃ x : α, (s : Set α) = { x }} :=
  isTopologicalBasis_of_isOpen_of_nhds (fun _ _ => isOpen_discrete _) fun x _ hx _ =>
    ⟨{ x }, ⟨x, rfl⟩, mem_singleton x, singleton_subset_iff.2 hx⟩

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