Commit 2026-10-17 12:17 e055050c

refactor(Analysis/Convex/Caratheodory): refactor Caratheodory's theorem using strong induction (#44863) convexHull_eq_union (Caratheodory's theorem) was proved using Caratheodory.minCardFinsetOfMemConvexHull, a chosen finest of minimal cardinality whose convex hull contains x. I replace this with a direct proof using Finset.strongInduction. This makes Caratheodory.minCardFinsetOfMemConvexHull no longer necessary, hence it can become deprecated. This does lose the functionality of getting a finest of minimal cardinality, but I don't think that should be needed anyway. The important point of the Caratheodory's theorem is that there exists an affinely independent subset. I'm also doing a small golf in the proof of eq_pos_convex_span_of_mem_convexHull and replace Sort (u + 1) with Type u.