affineIndependent_of_subsingleton

English

If the index set ι has at most one element, any p: ι → P is affinely independent.

Русский

Если индексное множество содержит не более одной точки, то любая функция p: ι → P аффинно независима.

LaTeX

$$AffineIndependent k p$$

Lean4

/-- A family with at most one point is affinely independent. -/
theorem affineIndependent_of_subsingleton [Subsingleton ι] (p : ι → P) : AffineIndependent k p := fun _ _ h _ i hi =>
  Fintype.eq_of_subsingleton_of_sum_eq h i hi

Похожие утверждения