Theorems · Definition · algebraic topology

Bundle.Trivialization.prod

{B : Type u_1} →
  [inst : TopologicalSpace B] →
    {F₁ : Type u_2} →
      [inst_1 : TopologicalSpace F₁] →
        {E₁ : B → Type u_3} →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] →
            {F₂ : Type u_4} →
              [inst_3 : TopologicalSpace F₂] →
                {E₂ : B → Type u_5} →
                  [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] →
                    Bundle.Trivialization F₁ Bundle.TotalSpace.proj →
                      Bundle.Trivialization F₂ Bundle.TotalSpace.proj →
                        [(x : B) → Zero (E₁ x)] →
                          [(x : B) → Zero (E₂ x)] → Bundle.Trivialization (F₁ × F₂) Bundle.TotalSpace.proj

Given trivializations e₁, e₂ for bundle types E₁, E₂ over a base B, the induced trivialization for the fiberwise product of E₁ and E₂, whose base set is e₁.baseSet ∩ e₂.baseSet.

Defined in

Mathlib.Topology.FiberBundle.Constructions

Cited by

12 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceZeroZero