isQuasiSeparated_univ — Mathlib

English

Let α be a topological space which is quasi-separated. Then the universal subset univ ⊆ α is quasi-separated.

Русский

Пусть α — топологическое пространство, которое квазиразделимо. Тогда множество-univ ⊆ α является квазиразделимым.

LaTeX

$$$IsQuasiSeparated(\\mathrm{univ} : Set\\alpha)$$$

Lean4

theorem isQuasiSeparated_univ {α : Type*} [TopologicalSpace α] [QuasiSeparatedSpace α] :
    IsQuasiSeparated (Set.univ : Set α) :=
  isQuasiSeparated_univ_iff.mpr inferInstance

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