α : Type u_1
β : Type ?u.15502
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated Set.univ
α : Type u_1
β : Type ?u.15502
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ IsQuasiSeparated s ↔ QuasiSeparatedSpace ↑s
rw [← isQuasiSeparated_univ_iff]
case h.e'_1.h.e'_3
α : Type u_1
β : Type ?u.15502
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ s = Subtype.val '' Set.univ
α : Type u_1
β : Type ?u.15502
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ IsQuasiSeparated s ↔ IsQuasiSeparated Set.univ
convert (hs.openEmbedding_subtype_val.isQuasiSeparated_iff (s := Set.univ)).symm
no goals
case h.e'_1.h.e'_3
α : Type u_1
β : Type ?u.15502
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
hs : IsOpen s
⊢ s = Subtype.val '' Set.univ
simp