finite_of_fin_dim_affineIndependent

English

If the ambient space V is finite-dimensional, then any affine-independent family indexed by ι is finite.

Русский

Если пространство V конечномерно, то любая аффинно независимая семейство точек, индексированная ι, конечно по количеству элементов.

LaTeX

$$$[\text{FiniteDimensional}_k V] \Rightarrow (\text{AffineIndependent}_k p) \Rightarrow \text{Finite } ι$$$

Lean4

/-- An affine-independent family of points in a finite-dimensional affine space is finite. -/
theorem finite_of_fin_dim_affineIndependent [FiniteDimensional k V] {p : ι → P} (hi : AffineIndependent k p) :
    Finite ι := by
  nontriviality ι; inhabit ι
  rw [affineIndependent_iff_linearIndependent_vsub k p default] at hi
  letI : IsNoetherian k V := IsNoetherian.iff_fg.2 inferInstance
  exact (Set.finite_singleton default).finite_of_compl (Set.finite_coe_iff.1 hi.finite_of_isNoetherian)

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