𝕜 : Type u_3
E : Type u_2
M : Type u_1
H : Type u_4
E' : Type ?u.135524
M' : Type ?u.135527
H' : Type ?u.135530
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s t : Set M
⊢ ContinuousOn (fun x => ↑(LocalEquiv.symm (LocalEquiv.restr (LocalEquiv.symm f.toLocalEquiv) I.source)) x)
    (extend f I).source
𝕜 : Type u_3
E : Type u_2
M : Type u_1
H : Type u_4
E' : Type ?u.135524
M' : Type ?u.135527
H' : Type ?u.135530
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s t : Set M
⊢ ContinuousOn (↑(extend f I)) (extend f I).source
refine' I.continuous.comp_continuousOn _
𝕜 : Type u_3
E : Type u_2
M : Type u_1
H : Type u_4
E' : Type ?u.135524
M' : Type ?u.135527
H' : Type ?u.135530
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s t : Set M
⊢ ContinuousOn (fun x => ↑(LocalEquiv.symm (LocalEquiv.restr (LocalEquiv.symm f.toLocalEquiv) I.source)) x) f.source
𝕜 : Type u_3
E : Type u_2
M : Type u_1
H : Type u_4
E' : Type ?u.135524
M' : Type ?u.135527
H' : Type ?u.135530
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s t : Set M
⊢ ContinuousOn (fun x => ↑(LocalEquiv.symm (LocalEquiv.restr (LocalEquiv.symm f.toLocalEquiv) I.source)) x)
    (extend f I).source
rw [extend_source]
no goals
𝕜 : Type u_3
E : Type u_2
M : Type u_1
H : Type u_4
E' : Type ?u.135524
M' : Type ?u.135527
H' : Type ?u.135530
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
f f' : LocalHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
inst✝¹ : TopologicalSpace H'
inst✝ : TopologicalSpace M'
I' : ModelWithCorners 𝕜 E' H'
x : M
s t : Set M
⊢ ContinuousOn (fun x => ↑(LocalEquiv.symm (LocalEquiv.restr (LocalEquiv.symm f.toLocalEquiv) I.source)) x) f.source
exact f.continuousOn