English
Let s be any subset of E. Then conv(R,s) equals the union of conv(R,t) over all finite t ⊆ s.
Русский
Пусть s — произвольное подмножество E. Тогда выпуклая оболочка conv(R,s) равна объединению conv(R,t) по всем конечным t ⊆ s.
LaTeX
$$$\operatorname{conv}(R, s) = \bigcup_{t \subseteq s,\ t \text{ finite}} \operatorname{conv}(R, t)$$$
Lean4
theorem mk_mem_convexHull_prod {t : Set F} {x : E} {y : F} (hx : x ∈ convexHull R s) (hy : y ∈ convexHull R t) :
(x, y) ∈ convexHull R (s ×ˢ t) :=
by
rw [mem_convexHull_iff_exists_fintype] at hx hy ⊢
obtain ⟨ι, _, w, f, hw₀, hw₁, hfs, hf⟩ := hx
obtain ⟨κ, _, v, g, hv₀, hv₁, hgt, hg⟩ := hy
have h_sum : ∑ i : ι × κ, w i.1 * v i.2 = 1 := by rw [Fintype.sum_prod_type, ← sum_mul_sum, hw₁, hv₁, mul_one]
refine
⟨ι × κ, inferInstance, fun p => w p.1 * v p.2, fun p ↦ (f p.1, g p.2), fun p ↦ mul_nonneg (hw₀ _) (hv₀ _), h_sum,
fun p ↦ ⟨hfs _, hgt _⟩, ?_⟩
ext
·
simp_rw [Prod.fst_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_comm (w _), mul_smul, sum_comm (γ := ι), ←
Fintype.sum_smul_sum, hv₁, one_smul, hf]
· simp_rw [Prod.snd_sum, Prod.smul_mk, Fintype.sum_prod_type, mul_smul, ← Fintype.sum_smul_sum, hw₁, one_smul, hg]
