Theorems · Definition · convex and discrete geometry

ConvexIndependent

(𝕜 : Type u_1) →
  {E : Type u_2} →
    {ι : Type u_3} → [inst : Semiring 𝕜] → [PartialOrder 𝕜] → [inst_2 : AddCommGroup E] → [Module 𝕜 E] → (ι → E) → Prop

An indexed family is said to be convex independent if every point only belongs to convex hulls of sets containing it.

Defined in

Mathlib.Analysis.Convex.Independent

Cited by

15 results in Mathlib

Foundations

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

Assumes

SemiringPartialOrderAddCommGroupModule