ι : Type ?u.65338
B : Type u_1
F : Type u_3
X : Type ?u.65347
inst✝³ : TopologicalSpace X
E : B → Type u_2
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ Continuous TotalSpace.proj
ι : Type ?u.65338
B : Type u_1
F : Type u_3
X : Type ?u.65347
inst✝³ : TopologicalSpace X
E : B → Type u_2
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
⊢ Continuous TotalSpace.proj
letI := a.totalSpaceTopology
ι : Type ?u.65338
B : Type u_1
F : Type u_3
X : Type ?u.65347
inst✝³ : TopologicalSpace X
E : B → Type u_2
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
this✝ : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
this : FiberBundle F E := toFiberBundle a
⊢ Continuous TotalSpace.proj
ι : Type ?u.65338
B : Type u_1
F : Type u_3
X : Type ?u.65347
inst✝³ : TopologicalSpace X
E : B → Type u_2
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
this : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
⊢ Continuous TotalSpace.proj
letI := a.toFiberBundle
no goals
ι : Type ?u.65338
B : Type u_1
F : Type u_3
X : Type ?u.65347
inst✝³ : TopologicalSpace X
E : B → Type u_2
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
this✝ : TopologicalSpace (TotalSpace E) := totalSpaceTopology a
this : FiberBundle F E := toFiberBundle a
⊢ Continuous TotalSpace.proj
exact FiberBundle.continuous_proj F E