𝕜 : Type u_4
E : Type u_3
M : Type u_2
H : Type u_5
E' : Type ?u.146554
M' : Type ?u.146557
H' : Type ?u.146560
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
X : Type u_1
inst✝ : TopologicalSpace X
g : M → X
s : Set M
x : M
⊢ ContinuousWithinAt (g ∘ ↑(LocalEquiv.symm (extend f I))) (↑(LocalEquiv.symm (extend f I)) ⁻¹' s ∩ range ↑I)
      (↑(extend f I) x) ↔
    ContinuousWithinAt ((g ∘ ↑(LocalHomeomorph.symm f)) ∘ ↑(ModelWithCorners.symm I))
      (↑(ModelWithCorners.symm I) ⁻¹' (↑(LocalHomeomorph.symm f) ⁻¹' s) ∩ range ↑I) (↑I (↑f x))
𝕜 : Type u_4
E : Type u_3
M : Type u_2
H : Type u_5
E' : Type ?u.146554
M' : Type ?u.146557
H' : Type ?u.146560
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
X : Type u_1
inst✝ : TopologicalSpace X
g : M → X
s : Set M
x : M
⊢ ContinuousWithinAt (g ∘ ↑(LocalEquiv.symm (extend f I))) (↑(LocalEquiv.symm (extend f I)) ⁻¹' s ∩ range ↑I)
      (↑(extend f I) x) ↔
    ContinuousWithinAt (g ∘ ↑(LocalHomeomorph.symm f)) (↑(LocalHomeomorph.symm f) ⁻¹' s) (↑f x)
rw [← I.symm_continuousWithinAt_comp_right_iff]
no goals
𝕜 : Type u_4
E : Type u_3
M : Type u_2
H : Type u_5
E' : Type ?u.146554
M' : Type ?u.146557
H' : Type ?u.146560
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
X : Type u_1
inst✝ : TopologicalSpace X
g : M → X
s : Set M
x : M
⊢ ContinuousWithinAt (g ∘ ↑(LocalEquiv.symm (extend f I))) (↑(LocalEquiv.symm (extend f I)) ⁻¹' s ∩ range ↑I)
      (↑(extend f I) x) ↔
    ContinuousWithinAt ((g ∘ ↑(LocalHomeomorph.symm f)) ∘ ↑(ModelWithCorners.symm I))
      (↑(ModelWithCorners.symm I) ⁻¹' (↑(LocalHomeomorph.symm f) ⁻¹' s) ∩ range ↑I) (↑I (↑f x))
rfl