English
If the range of an indexing map p: ι → P is affinely independent over k and p is injective, then p is affinely independent.
Русский
Если множество значений отображения p: ι → P образует аффинную независимость над полем k и отображение p инъективно, то семейство p(ι) аффинно независимо.
LaTeX
$$$\\big(\\operatorname{AffineIndependent} k\\big( \\mathrm{incl}: \\mathrm{range}(p) \\to P \\big)\\big) \\to \\big(\\operatorname{Injective}(p)\\big) \\to \\operatorname{AffineIndependent} k p$$$
Lean4
/-- If the range of an injective indexed family of points is affinely
independent, so is that family. -/
theorem of_set_of_injective {p : ι → P} (ha : AffineIndependent k (fun x => x : Set.range p → P))
(hi : Function.Injective p) : AffineIndependent k p :=
ha.comp_embedding (⟨fun i => ⟨p i, Set.mem_range_self _⟩, fun _ _ h => hi (Subtype.mk_eq_mk.1 h)⟩ : ι ↪ Set.range p)
