Theorem: homeo_preserves_empty_interior (Sard/ObsoleteHelpers.lean)

State before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
s : Set α
h₂s : interior s = ∅
⊢ interior (⇑f '' s) = ∅
Tactic:
rw [← Homeomorph.image_interior, h₂s]
State after:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
s : Set α
h₂s : interior s = ∅
⊢ ⇑f '' ∅ = ∅

State before:
α β : Type
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α ≃ₜ β
s : Set α
h₂s : interior s = ∅
⊢ ⇑f '' ∅ = ∅
Tactic:
exact Set.image_empty ↑f
State after:
no goals