Theorems · Theorem · convex and discrete geometry

Pi.convexCombPair_apply

∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {ι : Type u_3}
  {X : ι → Type u_4} [inst_3 : (i : ι) → Convexity.ConvexSpace R (X i)] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b)
  (hab : a + b = 1) (f g : (i : ι) → X i) (i : ι),
  Convexity.convexCombPair a b ha hb hab f g i = Convexity.convexCombPair a b ha hb hab (f i) (g i)

Defined in

Mathlib.Geometry.Convex.ConvexSpace.Prod

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringPartialOrderIsStrictOrderedRingConvexity.ConvexSpace