Convex hulls with a point adjoined

Mathlib's convexHull_insert writes the convex hull of insert a s as the convex join of {a} with the convex hull of s, provided s is nonempty. This file states the membership form with no nonemptiness hypothesis: a point of the convex hull of insert a s is either a itself or lies on a segment from a to a point of the convex hull of s (TauCeti.mem_convexHull_insert).

theorem TauCeti.mem_convexHull_insert {𝕜 : Type u_1} {E : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {s : Set E} {a x : E} : x ∈ (convexHull 𝕜) (insert a s) ↔ x = a ∨ ∃ y ∈ (convexHull 𝕜) s, x ∈ segment 𝕜 a y

A point of the convex hull of insert a s is either a or lies on a segment from a to a point of the convex hull of s. Unlike convexHull_insert, this needs no nonemptiness of s.