English
If S, T, U are subsets, then convexJoin is commutative on the left in the sense that swapping S with T inside a nested convexJoin does not change the result:\nconvexJoin(S, convexJoin(T, U)) = convexJoin(T, convexJoin(S, U)).
Русский
Для подмножеств S, T, U операция convexJoin слева коммутирует: convexJoin(S, convexJoin(T, U)) = convexJoin(T, convexJoin(S, U)).
LaTeX
$$$\\operatorname{convexJoin}_{\\mathbb{K}}(S,\\operatorname{convexJoin}_{\\mathbb{K}}(T,U))=\\operatorname{convexJoin}_{\\mathbb{K}}(T,\\operatorname{convexJoin}_{\\mathbb{K}}(S,U)).$$$
Lean4
theorem convexJoin_left_comm (s t u : Set E) : convexJoin 𝕜 s (convexJoin 𝕜 t u) = convexJoin 𝕜 t (convexJoin 𝕜 s u) :=
by simp_rw [← convexJoin_assoc, convexJoin_comm]
