Theorems · Definition · algebraic topology

Bundle.Trivial.homeomorphProd

(B : Type u_1) →
  (F : Type u_2) →
    [inst : TopologicalSpace B] → [inst_1 : TopologicalSpace F] → Bundle.TotalSpace F (Bundle.Trivial B F) ≃ₜ B × F

Homeomorphism between the total space of the trivial bundle and the Cartesian product.

Defined in: Mathlib.Topology.FiberBundle.Constructions
Cited by: 3 results in Mathlib
Foundations: Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace TopologicalSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
Bundle.TotalSpacestatement · cited by 766
Homeomorphstatement · cited by 725
Bundle.Trivialstatement · cited by 20
Bundle.TotalSpace.toProdproof · cited by 11
Equiv.toHomeomorphOfIsInducingproof · cited by 8
Bundle.Trivial.isInducing_toProdproof · cited by 0

Cited by4

Results whose statement or proof uses this declaration.

Bundle.Trivial.trivializationproof · cited by 17
Bundle.Trivial.homeomorphProd_symm_apply_projstatement and proof · cited by 0
Bundle.Trivial.homeomorphProd_symm_apply_sndstatement and proof · cited by 0
Bundle.Trivial.homeomorphProd_applystatement and proof · cited by 0