α : Type u_1
β : Type u_2
γ : Type ?u.225202
δ : Type ?u.225205
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
α : Type u_1
β : Type u_2
γ : Type ?u.225202
δ : Type ?u.225205
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
⊢ IsClosedMap f
intro s hs
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.225202
δ : Type ?u.225205
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
s : Set α
hs : IsClosed s
h2s : s = ∅
⊢ IsClosed (f '' s)

case inr
α : Type u_1
β : Type u_2
γ : Type ?u.225202
δ : Type ?u.225205
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
s : Set α
hs : IsClosed s
h2s : Set.Nonempty s
⊢ IsClosed (f '' s)
α : Type u_1
β : Type u_2
γ : Type ?u.225202
δ : Type ?u.225205
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
cases' eq_empty_or_nonempty s with h2s h2s
no goals
case inl
α : Type u_1
β : Type u_2
γ : Type ?u.225202
δ : Type ?u.225205
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
s : Set α
hs : IsClosed s
h2s : s = ∅
⊢ IsClosed (f '' s)
simp_rw [h2s, image_empty, isClosed_empty]
no goals
case inr
α : Type u_1
β : Type u_2
γ : Type ?u.225202
δ : Type ?u.225205
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h : ∀ (s : Set α), IsClosed s → Set.Nonempty s → IsClosed (f '' s)
s : Set α
hs : IsClosed s
h2s : Set.Nonempty s
⊢ IsClosed (f '' s)
exact h s hs h2s