mathlib3

ceb9da60 - feat(analysis/convex/caratheodory): strengthen Caratheodory's lemma to provide affine independence (#8892)

feat(analysis/convex/caratheodory): strengthen Caratheodory's lemma to provide affine independence (#8892) The changes here are: - Use hypothesis `¬ affine_independent ℝ (coe : t → E)` instead of `finrank ℝ E + 1 < t.card` - Drop no-longer-necessary `[finite_dimensional ℝ E]` assumption - Do not use a shrinking argument but start by choosing an appropriate subset of minimum cardinality via `min_card_finset_of_mem_convex_hull` - Provide a single alternative form of Carathéodory's lemma `eq_pos_convex_span_of_mem_convex_hull` - In the alternate form, define the explicit linear combination using elements parameterised by a new `fintype` rather than on the entire ambient space `E` (we thus avoid the issue of junk values outside of the relevant subset)