English
If an indexed family is affine independent, so is the corresponding set of points.
Русский
Если множество индексов образует аффинно независимое семейство, то и соответствующее множество точек независимо.
LaTeX
$$AffineIndependent k p → AffineIndependent k (fun x => x : Set.range p → P)$$
Lean4
/-- If an indexed family of points is affinely independent, so is the
corresponding set of points. -/
protected theorem range {p : ι → P} (ha : AffineIndependent k p) : AffineIndependent k (fun x => x : Set.range p → P) :=
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 ha.comp_embedding fe
ext
simp [fe, hf]
