Theorems · Theorem · convex and discrete geometry

mem_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)} {x : (i : ι) → E i}, (∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)) → x ∈ (convexHull 𝕜) (s.pi t)

Defined in

Mathlib.Analysis.Convex.Combination

Cited by

1 results in Mathlib

Foundations

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

Assumes

FiniteFieldLinearOrderIsStrictOrderedRingAddCommGroupModule