α : Type u_2
β : Type u_1
γ : Type ?u.198659
δ : Type ?u.198662
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
f' : β → α
h : Continuous f'
l_inv : LeftInverse f f'
r_inv : Function.RightInverse f f'
s : Set α
hs : IsClosed s
⊢ IsClosed (f' ⁻¹' s)
α : Type u_2
β : Type u_1
γ : Type ?u.198659
δ : Type ?u.198662
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
f' : β → α
h : Continuous f'
l_inv : LeftInverse f f'
r_inv : Function.RightInverse f f'
s : Set α
hs : IsClosed s
⊢ IsClosed (f '' s)
rw [image_eq_preimage_of_inverse r_inv l_inv]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.198659
δ : Type ?u.198662
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
f' : β → α
h : Continuous f'
l_inv : LeftInverse f f'
r_inv : Function.RightInverse f f'
s : Set α
hs : IsClosed s
⊢ IsClosed (f' ⁻¹' s)
exact hs.preimage h