English
If S and T are convex subsets, then their convexJoin is convex.
Русский
Если S и T выпуклы, то их convexJoin выпукло.
LaTeX
$$$\\text{If } S,T \\subset E\\text{ with } S,T\\text{ convex, then } \\operatorname{convexJoin}_{\\mathbb{K}}(S,T)\\text{ is convex.}$$$
Lean4
protected theorem convexJoin (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (convexJoin 𝕜 s t) :=
by
simp only [Convex, StarConvex, convexJoin, mem_iUnion]
rintro _ ⟨x₁, hx₁, y₁, hy₁, a₁, b₁, ha₁, hb₁, hab₁, rfl⟩ _ ⟨x₂, hx₂, y₂, hy₂, a₂, b₂, ha₂, hb₂, hab₂, rfl⟩ p q hp hq
hpq
rcases hs.exists_mem_add_smul_eq hx₁ hx₂ (mul_nonneg hp ha₁) (mul_nonneg hq ha₂) with ⟨x, hxs, hx⟩
rcases ht.exists_mem_add_smul_eq hy₁ hy₂ (mul_nonneg hp hb₁) (mul_nonneg hq hb₂) with ⟨y, hyt, hy⟩
refine ⟨_, hxs, _, hyt, p * a₁ + q * a₂, p * b₁ + q * b₂, ?_, ?_, ?_, ?_⟩ <;> try positivity
· linear_combination p * hab₁ + q * hab₂ + hpq
· rw [hx, hy]
module
