English
Convex independence can be checked using finsets: p is convex independent iff for every finite set s, and every x, p x ∈ convHull(s.image p) implies x ∈ s.
Русский
Контроль конвексивной независимости можно свести к финсетам: p конвексиво независимо, если для каждого конечного множества s и любого x выполняется p x ∈ convHull(s.image p) ⇒ x ∈ s.
LaTeX
$$$\\text{ConvexIndependent}_{\\mathbb{k}}(p) \\iff \\forall s \\; (x:\\iota), p x ∈ convHull_{\\mathbb{k}}(s.image\,p) \\Rightarrow x ∈ s$$$
Lean4
/-- To check convex independence, one only has to check finsets thanks to Carathéodory's theorem. -/
theorem convexIndependent_iff_finset {p : ι → E} :
ConvexIndependent 𝕜 p ↔ ∀ (s : Finset ι) (x : ι), p x ∈ convexHull 𝕜 (s.image p : Set E) → x ∈ s :=
by
refine ⟨fun hc s x hx => hc s x ?_, fun h s x hx => ?_⟩
· rwa [Finset.coe_image] at hx
have hp : Injective p := by
rintro a b hab
rw [← mem_singleton]
refine h { b } a ?_
rw [hab, image_singleton, coe_singleton, convexHull_singleton]
exact Set.mem_singleton _
rw [convexHull_eq_union_convexHull_finite_subsets] at hx
simp_rw [Set.mem_iUnion] at hx
obtain ⟨t, ht, hx⟩ := hx
rw [← hp.mem_set_image]
refine ht ?_
suffices x ∈ t.preimage p hp.injOn by rwa [mem_preimage, ← mem_coe] at this
refine h _ x ?_
rwa [t.image_preimage p hp.injOn, filter_true_of_mem]
exact fun y hy => s.image_subset_range p (ht <| mem_coe.2 hy)
