Theorems · Inductive type · algebraic topology

Bundle.Trivialization

{B : Type u_1} →
  (F : Type u_2) →
    {Z : Type u_4} →
      [TopologicalSpace B] → [TopologicalSpace F] → [TopologicalSpace Z] → (Z → B) → Type (max (max u_1 u_2) u_4)

A structure extending open partial homeomorphisms, defining a local trivialization of a projection proj : Z → B with fiber F, as an open partial homeomorphism between Z and B × F defined between two sets of the form proj ⁻¹' baseSet and baseSet × F, acting trivially on the first coordinate.

Defined in

Mathlib.Topology.FiberBundle.Trivialization

Cited by

324 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpace