Theorems · Inductive type · algebraic topology

Bundle.Pretrivialization.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 : AddCommMonoid F] →
                [Module R F] →
                  [inst_5 : (x : B) → AddCommMonoid (E x)] →
                    [(x : B) → Module R (E x)] → Bundle.Pretrivialization F Bundle.TotalSpace.proj → Prop

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

Defined in

Mathlib.Topology.VectorBundle.Basic

Cited by

21 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

SemiringTopologicalSpaceTopologicalSpaceAddCommMonoidModuleAddCommMonoidModule