B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ ≤ induced (Pullback.lift f) inst✝
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
f✝ : B' → B
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace E)
f : B' → B
⊢ Continuous (Pullback.lift f)
rw [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, 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)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ ≤ induced (Pullback.lift f) inst✝
exact inf_le_right