hasSeparatingCover_empty_right — Mathlib

English

For every s there exists a separating cover with the right side equal to the empty set.

Русский

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

LaTeX

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

Lean4

theorem hasSeparatingCover_empty_right (s : Set X) : HasSeparatingCover s ∅ :=
  ⟨fun _ ↦ univ, (subset_univ s).trans univ.iUnion_const.symm.subset, fun _ ↦ ⟨isOpen_univ, by apply disjoint_empty⟩⟩

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