Theorems · Theorem · convex and discrete geometry

convexHull_pi

∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [Finite ι] [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : (i : ι) → AddCommGroup (E i)] [inst_4 : (i : ι) → Module 𝕜 (E i)] (s : Set ι)
  (t : (i : ι) → Set (E i)), (convexHull 𝕜) (s.pi t) = s.pi fun i => (convexHull 𝕜) (t i)

Defined in

Mathlib.Analysis.Convex.Combination

Cited by

0 results in Mathlib

Foundations

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

Assumes

FiniteFieldLinearOrderIsStrictOrderedRingAddCommGroupModule