isTopologicalBasis_empty — Mathlib

English

The empty family of sets forms a topological basis for α if and only if α is empty.

Русский

Пусть пустой набор множеств образует топологический базис для пространства α тогда и только тогда, когда α пусто.

LaTeX

$$$\\mathsf{IsTopologicalBasis}(\\emptyset) \\iff \\mathrm{IsEmpty}(\\alpha)$$$

Lean4

@[simp]
theorem isTopologicalBasis_empty : IsTopologicalBasis (∅ : Set (Set α)) ↔ IsEmpty α
    where
  mp h := by simpa using h.sUnion_eq.symm
  mpr h := ⟨by simp, by simp [Set.univ_eq_empty_iff.2], Subsingleton.elim ..⟩

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