Theorems · Definition · convex and discrete geometry

convexJoin

(𝕜 : Type u_2) →
  {E : Type u_3} →
    [inst : Semiring 𝕜] → [PartialOrder 𝕜] → [inst_2 : AddCommMonoid E] → [Module 𝕜 E] → Set E → Set E → Set E

The join of two sets is the union of the segments joining them. This can be interpreted as the topological join, but within the original space.

Defined in

Mathlib.Analysis.Convex.Join

Cited by

31 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

SemiringPartialOrderAddCommMonoidModule