Theorems · Definition · convex and discrete geometry

Convexity.ConvexSpace.AffineMap.comp

{R : Type u_1} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      [inst_2 : IsStrictOrderedRing R] →
        {X : Type u_2} →
          {Y : Type u_3} →
            {Z : Type u_4} →
              [inst_3 : Convexity.ConvexSpace R X] →
                [inst_4 : Convexity.ConvexSpace R Y] →
                  [inst_5 : Convexity.ConvexSpace R Z] →
                    Convexity.ConvexSpace.AffineMap R Y Z →
                      Convexity.ConvexSpace.AffineMap R X Y → Convexity.ConvexSpace.AffineMap R X Z

The composition of bundled affine maps between convex spaces.

Defined in

Mathlib.Geometry.Convex.ConvexSpace.AffineMap

Cited by

5 results in Mathlib

Foundations

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

Assumes

PartialOrderSemiringIsStrictOrderedRingConvexity.ConvexSpaceConvexity.ConvexSpaceConvexity.ConvexSpace