no goals
α : Type u_1
β : Type u_2
γ : Type ?u.197449
δ : Type ?u.197452
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hs : ∀ (s : Set α), f '' interior s ⊆ interior (f '' s)
u : Set α
hu : IsOpen u
⊢ f '' u = f '' interior u
rw [hu.interior_eq]