𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑e
⊢ ∀ (s : Set E), IsOpen s → IsOpen (↑(symm e) ⁻¹' s)
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑e
⊢ Continuous ↑(symm e)
rw [continuous_def]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑e
s : Set E
hs : IsOpen s
⊢ IsOpen (↑(symm e) ⁻¹' s)
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑e
⊢ ∀ (s : Set E), IsOpen s → IsOpen (↑(symm e) ⁻¹' s)
intro s hs
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑e
s : Set E
hs : IsOpen s
⊢ IsOpen (↑e '' s)
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑e
s : Set E
hs : IsOpen s
⊢ IsOpen (↑(symm e) ⁻¹' s)
rw [← e.image_eq_preimage]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑↑e
s : Set E
hs : IsOpen s
⊢ IsOpen (↑↑e '' s)
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑e
s : Set E
hs : IsOpen s
⊢ IsOpen (↑e '' s)
rw [← e.coe_coe] at h⊢
no goals
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
f : E →L[𝕜] F
inst✝¹ : CompleteSpace F
inst✝ : CompleteSpace E
e : E ≃ₗ[𝕜] F
h : Continuous ↑↑e
s : Set E
hs : IsOpen s
⊢ IsOpen (↑↑e '' s)
exact ContinuousLinearMap.isOpenMap (𝕜 := 𝕜) ⟨↑e, h⟩ e.surjective s hs