ι : Type ?u.11181
B : Type u_1
F : Type u_4
X : Type u_3
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
E : B → Type u_2
inst✝² : TopologicalSpace (TotalSpace E)
inst✝¹ : (b : B) → TopologicalSpace (E b)
inst✝ : FiberBundle F E
f : X → TotalSpace E
x₀ : X
⊢ ContinuousWithinAt f univ x₀ ↔
    ContinuousWithinAt (fun x => TotalSpace.proj (f x)) univ x₀ ∧
      ContinuousWithinAt (fun x => (↑(trivializationAt F E (TotalSpace.proj (f x₀))) (f x)).snd) univ x₀
ι : Type ?u.11181
B : Type u_1
F : Type u_4
X : Type u_3
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
E : B → Type u_2
inst✝² : TopologicalSpace (TotalSpace E)
inst✝¹ : (b : B) → TopologicalSpace (E b)
inst✝ : FiberBundle F E
f : X → TotalSpace E
x₀ : X
⊢ ContinuousAt f x₀ ↔
    ContinuousAt (fun x => TotalSpace.proj (f x)) x₀ ∧
      ContinuousAt (fun x => (↑(trivializationAt F E (TotalSpace.proj (f x₀))) (f x)).snd) x₀
simp_rw [← continuousWithinAt_univ]
no goals
ι : Type ?u.11181
B : Type u_1
F : Type u_4
X : Type u_3
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace B
inst✝³ : TopologicalSpace F
E : B → Type u_2
inst✝² : TopologicalSpace (TotalSpace E)
inst✝¹ : (b : B) → TopologicalSpace (E b)
inst✝ : FiberBundle F E
f : X → TotalSpace E
x₀ : X
⊢ ContinuousWithinAt f univ x₀ ↔
    ContinuousWithinAt (fun x => TotalSpace.proj (f x)) univ x₀ ∧
      ContinuousWithinAt (fun x => (↑(trivializationAt F E (TotalSpace.proj (f x₀))) (f x)).snd) univ x₀
exact continuousWithinAt_totalSpace F f