α : Type u
t : TopologicalSpace α
s : Set α
inst✝ : SeparableSpace ↑s
this : IsSeparable (Subtype.val '' univ)
⊢ IsSeparable s
α : Type u
t : TopologicalSpace α
s : Set α
inst✝ : SeparableSpace ↑s
⊢ IsSeparable s
have : IsSeparable (((↑) : s → α) '' (univ : Set s)) :=
  (isSeparable_of_separableSpace _).image continuous_subtype_val
no goals
α : Type u
t : TopologicalSpace α
s : Set α
inst✝ : SeparableSpace ↑s
this : IsSeparable (Subtype.val '' univ)
⊢ IsSeparable s
simpa only [image_univ, Subtype.range_val_subtype] using this