convexJoin_comm

theorem convexJoin_comm : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E] (s t : Set E), convexJoin 𝕜 s t = convexJoin 𝕜 t s

The theorem `convexJoin_comm` states that for any two sets `s` and `t` of some type `E`, the convex join of `s` and `t` is equal to the convex join of `t` and `s`. This is under the conditions that `E` is an additive commutative monoid, `𝕜` is an ordered semiring, and a module structure over `E` with scalars from `𝕜` is defined. In simpler terms, the theorem is stating that the operation of taking the convex join of two sets is commutative, meaning the order of the sets does not change the result.

More concisely: For sets `s` and `t` in an additive commutative monoid `E` over an ordered semiring `𝕜` with a module structure, the convex joins `convS (s ++ t)` and `convS (t ++ s)` are equal.