English
For four sets S,T,U,V, the join of their pairwise joins satisfies\nconvexJoin( convexJoin(S,T), convexJoin(U,V) ) = convexJoin( convexJoin(S,U), convexJoin(T,V) ).
Русский
Для четырех множеств S,T,U,V верна симметрия выпуклого объединения: convexJoin( convexJoin(S,T), convexJoin(U,V) ) = convexJoin( convexJoin(S,U), convexJoin(T,V) ).
LaTeX
$$$\\operatorname{convexJoin}_{\\mathbb{K}}\\big(\\operatorname{convexJoin}_{\\mathbb{K}}(S,T),\\operatorname{convexJoin}_{\\mathbb{K}}(U,V)\\big)=\\operatorname{convexJoin}_{\\mathbb{K}}\\big(\\operatorname{convexJoin}_{\\mathbb{K}}(S,U),\\operatorname{convexJoin}_{\\mathbb{K}}(T,V)\\big).$$$
Lean4
theorem convexJoin_convexJoin_convexJoin_comm (s t u v : Set E) :
convexJoin 𝕜 (convexJoin 𝕜 s t) (convexJoin 𝕜 u v) = convexJoin 𝕜 (convexJoin 𝕜 s u) (convexJoin 𝕜 t v) := by
simp_rw [← convexJoin_assoc, convexJoin_right_comm]
