English
The convex independence of a family implies convex independence of the map to its range; in particular, the range map is convex independent when the original family is.
Русский
Конвексивная независимость семейства переносится на отображение к его диапазону.
LaTeX
$$$\\text{ConvexIndependent}_{\\mathbb{k}}(p) \\Rightarrow \\text{ConvexIndependent}_{\\mathbb{k}}\\bigl(\\mathrm{Subtype.val}:\\mathrm{range}(p)\\to E\\bigr)$$$
Lean4
/-- If an indexed family of points is convex independent, so is the corresponding set of points. -/
protected theorem range {p : ι → E} (hc : ConvexIndependent 𝕜 p) : ConvexIndependent 𝕜 ((↑) : Set.range p → E) :=
by
let f : Set.range p → ι := fun x => x.property.choose
have hf : ∀ x, p (f x) = x := fun x => x.property.choose_spec
let fe : Set.range p ↪ ι := ⟨f, fun x₁ x₂ he => Subtype.ext (hf x₁ ▸ hf x₂ ▸ he ▸ rfl)⟩
convert hc.comp_embedding fe
ext
rw [Embedding.coeFn_mk, comp_apply, hf]
