English
Let S, T, U be subsets of a vector space over a field 𝕜, and let convexJoin denote the join of two sets by convex combinations. Then the join is associative:\nIf one forms convexJoin( S, T ) and then convexJoin with U, the result equals forming convexJoin with S and convexJoin(T, U) instead.
Русский
Пусть S, T, U — подмножества векторного пространства над полем 𝕜, операция convexJoin обозначает объединение через выпуклые комбинации. Тогда выполняется ассоциативность:\nconvexJoin(S, convexJoin(T, U)) = convexJoin(convexJoin(S, T), U).
LaTeX
$$$\\operatorname{convexJoin}_{\\mathbb{K}}(\\operatorname{convexJoin}_{\\mathbb{K}}(S,T),U)=\\operatorname{convexJoin}_{\\mathbb{K}}(S,\\operatorname{convexJoin}_{\\mathbb{K}}(T,U)).$$$
Lean4
theorem convexJoin_assoc (s t u : Set E) : convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 s (convexJoin 𝕜 t u) :=
by
refine (convexJoin_assoc_aux _ _ _).antisymm ?_
simp_rw [convexJoin_comm s, convexJoin_comm _ u]
exact convexJoin_assoc_aux _ _ _
