case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.33913
δ : Type ?u.33916
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α → β
de : DenseEmbedding e
p : α → Prop
x : β
hx : x ∈ closure (e '' {x | p x})
⊢ { val := x, property := hx } ∈ closure (range (subtypeEmb p e)) ↔ { val := x, property := hx } ∈ univ
α : Type u_1
β : Type u_2
γ : Type ?u.33913
δ : Type ?u.33916
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α → β
de : DenseEmbedding e
p : α → Prop
⊢ closure (range (subtypeEmb p e)) = univ
ext ⟨x, hx⟩
case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.33913
δ : Type ?u.33916
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α → β
de : DenseEmbedding e
p : α → Prop
x : β
hx✝ : x ∈ closure (e '' {x | p x})
hx : x ∈ closure (range fun x => e ↑x)
⊢ { val := x, property := hx✝ } ∈ closure (range (subtypeEmb p e)) ↔ { val := x, property := hx✝ } ∈ univ
case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.33913
δ : Type ?u.33916
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α → β
de : DenseEmbedding e
p : α → Prop
x : β
hx : x ∈ closure (e '' {x | p x})
⊢ { val := x, property := hx } ∈ closure (range (subtypeEmb p e)) ↔ { val := x, property := hx } ∈ univ
rw [image_eq_range] at hx