# Documentation

Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle

# Maps equivariantly-homeomorphic to projection in a product #

This file contains the definition IsHomeomorphicTrivialFiberBundle F p, a Prop saying that a map p : Z → B between topological spaces is a "trivial fiber bundle" in the sense that there exists a homeomorphism h : Z ≃ₜ B × F such that proj x = (h x).1. This is an abstraction which is occasionally convenient in showing that a map is open, a quotient map, etc.

This material was formerly linked to the main definition of fiber bundles, but after a series of refactors, there is no longer a direct connection.

def IsHomeomorphicTrivialFiberBundle {B : Type u_1} (F : Type u_2) {Z : Type u_3} [] [] [] (proj : ZB) :

A trivial fiber bundle with fiber F over a base B is a space Z projecting on B for which there exists a homeomorphism to B × F that sends proj to Prod.fst.

Instances For
theorem IsHomeomorphicTrivialFiberBundle.proj_eq {B : Type u_1} {F : Type u_2} {Z : Type u_3} [] [] [] {proj : ZB} (h : ) :
e, proj = Prod.fst e
theorem IsHomeomorphicTrivialFiberBundle.surjective_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} [] [] [] {proj : ZB} [] (h : ) :

The projection from a trivial fiber bundle to its base is surjective.

theorem IsHomeomorphicTrivialFiberBundle.continuous_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} [] [] [] {proj : ZB} (h : ) :

The projection from a trivial fiber bundle to its base is continuous.

theorem IsHomeomorphicTrivialFiberBundle.isOpenMap_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} [] [] [] {proj : ZB} (h : ) :

The projection from a trivial fiber bundle to its base is open.

theorem IsHomeomorphicTrivialFiberBundle.quotientMap_proj {B : Type u_1} {F : Type u_2} {Z : Type u_3} [] [] [] {proj : ZB} [] (h : ) :

The projection from a trivial fiber bundle to its base is open.

The first projection in a product is a trivial fiber bundle.

The second projection in a product is a trivial fiber bundle.