B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
f : B' → B
x : B'
⊢ instForAllTopologicalSpacePullback E f x ≤ induced (fun x_1 => Pullback.lift f { fst := x, snd := x_1 }) inst✝⁴
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
f : B' → B
x : B'
⊢ Continuous (totalSpaceMk x)
simp only [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, induced_compose,
  induced_inf, Function.comp, totalSpaceMk, TotalSpace.proj, induced_const, top_inf_eq,
  pullbackTopology_def]
no goals
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝⁵ : TopologicalSpace B'
inst✝⁴ : TopologicalSpace (TotalSpace E)
inst✝³ : TopologicalSpace F
inst✝² : TopologicalSpace B
inst✝¹ : (x : B) → TopologicalSpace (E x)
inst✝ : FiberBundle F E
f : B' → B
x : B'
⊢ instForAllTopologicalSpacePullback E f x ≤ induced (fun x_1 => Pullback.lift f { fst := x, snd := x_1 }) inst✝⁴
exact le_of_eq (FiberBundle.totalSpaceMk_inducing F E (f x)).induced