English
Let s,t be subsets of the real numbers. The convex hull of the set { x + i y : x ∈ s, y ∈ t } (i.e., the real-imaginary product) equals the product of the convex hulls: { a + i b : a ∈ conv(s), b ∈ conv(t) }.
Русский
Пусть s,t ⊆ ℝ. Выпуклая оболочка множества { x + i y : x ∈ s, y ∈ t } по реальной оси равна произведению выпуклых оболочек: { a + i b : a ∈ conv(s), b ∈ conv(t) }.
LaTeX
$$$\\operatorname{conv}_{\\mathbb{R}}\\{ x+iy : x \\in s,\\ y \\in t\\} = \\{ a+ib : a \\in \\operatorname{conv}_{\\mathbb{R}}(s),\\ b \\in \\operatorname{conv}_{\\mathbb{R}}(t) \\}$$$
Lean4
/-- A version of `convexHull_prod` for `Set.reProdIm`. -/
theorem convexHull_reProdIm (s t : Set ℝ) : convexHull ℝ (s ×ℂ t) = convexHull ℝ s ×ℂ convexHull ℝ t :=
calc
convexHull ℝ (equivRealProdLm ⁻¹' (s ×ˢ t)) = equivRealProdLm ⁻¹' convexHull ℝ (s ×ˢ t) := by
simpa only [← LinearEquiv.image_symm_eq_preimage] using
((equivRealProdLm.symm.toLinearMap).image_convexHull (s ×ˢ t)).symm
_ = convexHull ℝ s ×ℂ convexHull ℝ t := by rw [convexHull_prod]; rfl
