convexJoin_right_comm — Mathlib

English

Symmetric role of left and right arguments in convexJoin: convexJoin( convexJoin(S,T), U ) = convexJoin( convexJoin(S,U), T ).

Русский

Коммутативность convexJoin справа: convexJoin( convexJoin(S,T), U ) = convexJoin( convexJoin(S,U), T ).

LaTeX

$$$\\operatorname{convexJoin}_{\\mathbb{K}}(\\operatorname{convexJoin}_{\\mathbb{K}}(S,T),U)=\\operatorname{convexJoin}_{\\mathbb{K}}(\\operatorname{convexJoin}_{\\mathbb{K}}(S,U),T).$$$

Lean4

theorem convexJoin_right_comm (s t u : Set E) : convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 s u) t :=
  by simp_rw [convexJoin_assoc, convexJoin_comm]

Похожие утверждения