α : Type u_2
β : Type u_3
γ : Type u_1
δ : Type ?u.103511
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
h : f ⁻¹' e.source = univ
⊢ ContinuousOn f univ ↔ ContinuousOn (↑e ∘ f) univ
α : Type u_2
β : Type u_3
γ : Type u_1
δ : Type ?u.103511
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
h : f ⁻¹' e.source = univ
⊢ Continuous f ↔ Continuous (↑e ∘ f)
simp only [continuous_iff_continuousOn_univ]
no goals
α : Type u_2
β : Type u_3
γ : Type u_1
δ : Type ?u.103511
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
f : γ → α
h : f ⁻¹' e.source = univ
⊢ ContinuousOn f univ ↔ ContinuousOn (↑e ∘ f) univ
exact e.continuousOn_iff_continuousOn_comp_left (Eq.symm h).subset