convexJoin_union_left — Mathlib

English

convexJoin 𝕜 (s1 ∪ s2) t = convexJoin 𝕜 s1 t ∪ convexJoin 𝕜 s2 t.

Русский

convexJoin 𝕜 (s1 ∪ s2) t = convexJoin 𝕜 s1 t ∪ convexJoin 𝕜 s2 t.

LaTeX

$$$ convexJoin 𝕜 (s_1 \cup s_2) t = convexJoin 𝕜 s_1 t \cup convexJoin 𝕜 s_2 t $$$

Lean4

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

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