[GOAL]
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace Z
proj : Z → B
inst✝ : Nonempty F
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ Function.Surjective proj
[PROOFSTEP]
obtain ⟨e, rfl⟩ := h.proj_eq
[GOAL]
case intro
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty F
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ↑e)
⊢ Function.Surjective (Prod.fst ∘ ↑e)
[PROOFSTEP]
exact Prod.fst_surjective.comp e.surjective
[GOAL]
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
proj : Z → B
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ Continuous proj
[PROOFSTEP]
obtain ⟨e, rfl⟩ := h.proj_eq
[GOAL]
case intro
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ↑e)
⊢ Continuous (Prod.fst ∘ ↑e)
[PROOFSTEP]
exact continuous_fst.comp e.continuous
[GOAL]
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
proj : Z → B
h : IsHomeomorphicTrivialFiberBundle F proj
⊢ IsOpenMap proj
[PROOFSTEP]
obtain ⟨e, rfl⟩ := h.proj_eq
[GOAL]
case intro
B : Type u_1
F : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : TopologicalSpace Z
e : Z ≃ₜ B × F
h : IsHomeomorphicTrivialFiberBundle F (Prod.fst ∘ ↑e)
⊢ IsOpenMap (Prod.fst ∘ ↑e)
[PROOFSTEP]
exact isOpenMap_fst.comp e.isOpenMap
