α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.99648
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
⊢ (∀ (x : β), x ∈ s → ContinuousWithinAt f s x) ↔
    ∀ (x : β), x ∈ s → ContinuousWithinAt (f ∘ ↑e) (↑(LocalHomeomorph.symm e) '' s) (↑(LocalHomeomorph.symm e) x)
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.99648
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
⊢ ContinuousOn f s ↔ ContinuousOn (f ∘ ↑e) (e.source ∩ ↑e ⁻¹' s)
simp only [← e.symm_image_eq_source_inter_preimage h, ContinuousOn, ball_image_iff]
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.99648
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
x : β
hx : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑(LocalHomeomorph.symm e) '' s) (↑(LocalHomeomorph.symm e) x)
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.99648
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
⊢ (∀ (x : β), x ∈ s → ContinuousWithinAt f s x) ↔
    ∀ (x : β), x ∈ s → ContinuousWithinAt (f ∘ ↑e) (↑(LocalHomeomorph.symm e) '' s) (↑(LocalHomeomorph.symm e) x)
refine' forall₂_congr fun x hx => _
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.99648
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
x : β
hx : x ∈ s
⊢ e.source ∈ 𝓝 (↑(LocalHomeomorph.symm e) x)
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.99648
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
x : β
hx : x ∈ s
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ∘ ↑e) (↑(LocalHomeomorph.symm e) '' s) (↑(LocalHomeomorph.symm e) x)
rw [e.continuousWithinAt_iff_continuousWithinAt_comp_right (h hx),
  e.symm_image_eq_source_inter_preimage h, inter_comm, continuousWithinAt_inter]
no goals
α : Type u_2
β : Type u_1
γ : Type u_3
δ : Type ?u.99648
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : β → γ
s : Set β
h : s ⊆ e.target
x : β
hx : x ∈ s
⊢ e.source ∈ 𝓝 (↑(LocalHomeomorph.symm e) x)
exact IsOpen.mem_nhds e.open_source (e.map_target (h hx))