Theorems · Inductive type · algebraic topology

Bundle.Trivialization.IsLinear

(R : Type u_1) →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : Semiring R] →
          [inst_1 : TopologicalSpace F] →
            [inst_2 : TopologicalSpace B] →
              [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] →
                [inst_4 : AddCommMonoid F] →
                  [Module R F] →
                    [inst_6 : (x : B) → AddCommMonoid (E x)] →
                      [(x : B) → Module R (E x)] → Bundle.Trivialization F Bundle.TotalSpace.proj → Prop

A mixin class for Bundle.Trivialization, stating that a trivialization is fiberwise linear with respect to given module structures on its fibers and the model fiber.

Defined in

Mathlib.Topology.VectorBundle.Basic

Cited by

70 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

SemiringTopologicalSpaceTopologicalSpaceTopologicalSpaceAddCommMonoidModuleAddCommMonoidModule