Theorems · Theorem · convex and discrete geometry

Convexity.ConvexSpace.AffineMap.assoc

∀ {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} {T : Type u_5} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  [inst_5 : Convexity.ConvexSpace R Z] [inst_6 : Convexity.ConvexSpace R T] (f₁ : Convexity.ConvexSpace.AffineMap R Z T)
  (f₂ : Convexity.ConvexSpace.AffineMap R Y Z) (f₃ : Convexity.ConvexSpace.AffineMap R X Y),
  (f₁.comp f₂).comp f₃ = f₁.comp (f₂.comp f₃)

Defined in

Mathlib.Geometry.Convex.ConvexSpace.AffineMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

PartialOrderSemiringIsStrictOrderedRingConvexity.ConvexSpaceConvexity.ConvexSpaceConvexity.ConvexSpaceConvexity.ConvexSpace