α : Type ?u.175524
β : Type u_1
γ : Type ?u.175530
δ : Type ?u.175533
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_2
ι : Type ?u.175548
f : κ → β
g : β → γ
hf : DenseRange f
s : Set β
hs : IsOpen s
⊢ s ⊆ closure (s ∩ range f)
α : Type ?u.175524
β : Type u_1
γ : Type ?u.175530
δ : Type ?u.175533
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_2
ι : Type ?u.175548
f : κ → β
g : β → γ
hf : DenseRange f
s : Set β
hs : IsOpen s
⊢ s ⊆ closure (f '' (f ⁻¹' s))
rw [image_preimage_eq_inter_range]
no goals
α : Type ?u.175524
β : Type u_1
γ : Type ?u.175530
δ : Type ?u.175533
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
κ : Type u_2
ι : Type ?u.175548
f : κ → β
g : β → γ
hf : DenseRange f
s : Set β
hs : IsOpen s
⊢ s ⊆ closure (s ∩ range f)
exact hf.open_subset_closure_inter hs