Theorems · Definition · algebraic topology

FiberBundle.homeomorphAt

{B : Type u_2} →
  (F : Type u_3) →
    [inst : TopologicalSpace B] →
      [inst_1 : TopologicalSpace F] →
        (E : B → Type u_5) →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] →
            [inst_3 : (b : B) → TopologicalSpace (E b)] → [FiberBundle F E] → (b : B) → E b ≃ₜ F

An arbitrary homeomorphism between any fiber and the model fiber. This is useful to transfer topological properties of the model fiber.

Defined in

Mathlib.Topology.FiberBundle.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceFiberBundle