isQuasiSeparated_iff_quasiSeparatedSpace

English

If s is open, then IsQuasiSeparated s is equivalent to the corresponding subspace QuasiSeparatedSpace on s.

Русский

Если множество s открыто, то IsQuasiSeparated s эквивалентно тому, что подпространство на s квазиразделимо.

LaTeX

$$IsOpen(s) \\Rightarrow IsQuasiSeparated s \\leftrightarrow QuasiSeparatedSpace s$$

Lean4

theorem isQuasiSeparated_iff_quasiSeparatedSpace (s : Set α) (hs : IsOpen s) :
    IsQuasiSeparated s ↔ QuasiSeparatedSpace s :=
  by
  rw [← isQuasiSeparated_univ_iff]
  convert (hs.isOpenEmbedding_subtypeVal.isQuasiSeparated_iff (s := Set.univ)).symm
  simp

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