Theorems · Inductive type · algebraic topology

VectorBundleCore

(R : Type u_1) →
  (B : Type u_2) →
    (F : Type u_3) →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [NormedSpace R F] → [TopologicalSpace B] → Type u_5 → Type (max (max u_2 u_3) u_5)

Analogous construction of FiberBundleCore for vector bundles. This construction gives a way to construct vector bundles from a structure registering how trivialization changes act on fibers.

Defined in

Mathlib.Topology.VectorBundle.Basic

Cited by

38 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceTopologicalSpace