hasSeparatingCover_empty_left — Mathlib

English

For every subset s of X there exists a separating cover with the left component equal to the empty set.

Русский

Для любого подмножества s пространства X существует разделяющее покрытие, левая часть которого равна пустому множеству.

LaTeX

$$$ \mathrm{HasSeparatingCover}(\emptyset, s) $$$

Lean4

theorem hasSeparatingCover_empty_left (s : Set X) : HasSeparatingCover ∅ s :=
  ⟨fun _ ↦ ∅, empty_subset (⋃ _, ∅), fun _ ↦ ⟨isOpen_empty, by simp only [closure_empty, empty_disjoint]⟩⟩

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