𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_2
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ I.target = ↑I '' I.source
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_2
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ I.target = range ↑I
rw [← image_univ, ← I.source_eq]
no goals
𝕜 : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_2
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
⊢ I.target = ↑I '' I.source
exact I.image_source_eq_target.symm