convexJoin_union_right — Mathlib

English

convexJoin 𝕜 s (t1 ∪ t2) = convexJoin 𝕜 s t1 ∪ convexJoin 𝕜 s t2.

Русский

convexJoin 𝕜 s (t1 ∪ t2) = convexJoin 𝕜 s t1 ∪ convexJoin 𝕜 s t2.

LaTeX

$$$ convexJoin 𝕜 s (t_1 \cup t_2) = convexJoin 𝕜 s t_1 \cup convexJoin 𝕜 s t_2 $$$

Lean4

@[simp]
theorem convexJoin_union_right (s t₁ t₂ : Set E) : convexJoin 𝕜 s (t₁ ∪ t₂) = convexJoin 𝕜 s t₁ ∪ convexJoin 𝕜 s t₂ :=
  by simp_rw [convexJoin_comm s, convexJoin_union_left]

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