α : Type u_1
β : Type u_2
γ : Type ?u.226053
δ : Type ?u.226056
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
α : Type u_1
β : Type u_2
γ : Type ?u.226053
δ : Type ?u.226056
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
⊢ IsClosedMap f
intro s hs
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.226053
δ : Type ?u.226056
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
t : Set β
ht : IsClosed t
hs : IsClosed (f ⁻¹' t)
⊢ IsClosed (f '' (f ⁻¹' t))
α : Type u_1
β : Type u_2
γ : Type ?u.226053
δ : Type ?u.226056
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
rcases hf.isClosed_iff.1 hs with ⟨t, ht, rfl⟩
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.226053
δ : Type ?u.226056
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
t : Set β
ht : IsClosed t
hs : IsClosed (f ⁻¹' t)
⊢ IsClosed (t ∩ range f)
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.226053
δ : Type ?u.226056
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
t : Set β
ht : IsClosed t
hs : IsClosed (f ⁻¹' t)
⊢ IsClosed (f '' (f ⁻¹' t))
rw [image_preimage_eq_inter_range]
no goals
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.226053
δ : Type ?u.226056
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Inducing f
h : IsClosed (range f)
t : Set β
ht : IsClosed t
hs : IsClosed (f ⁻¹' t)
⊢ IsClosed (t ∩ range f)
exact ht.inter h