case induced
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
⊢ Pullback.TotalSpace.topologicalSpace E f = induced (pullbackTotalSpaceEmbedding f) instTopologicalSpaceProd
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
⊢ Inducing (pullbackTotalSpaceEmbedding f)
constructor
case induced
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 (Prod.fst ∘ pullbackTotalSpaceEmbedding f) inst✝¹ ⊓ induced (Prod.snd ∘ pullbackTotalSpaceEmbedding f) inst✝
case induced
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
⊢ Pullback.TotalSpace.topologicalSpace E f = induced (pullbackTotalSpaceEmbedding f) instTopologicalSpaceProd
simp_rw [instTopologicalSpaceProd, induced_inf, induced_compose,
  Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]
no goals
case induced
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 (Prod.fst ∘ pullbackTotalSpaceEmbedding f) inst✝¹ ⊓ induced (Prod.snd ∘ pullbackTotalSpaceEmbedding f) inst✝
rfl