finite_set_of_fin_dim_affineIndependent

English

An affine-independent subset of a finite-dimensional affine space is finite.

Русский

Подмножество, аффинно независимое внутри конечномерного аффинного пространства, конечно по количеству элементов.

LaTeX

$$$[\text{FiniteDimensional}_k V] \Rightarrow (\text{AffineIndependent}_k f) \Rightarrow f\text{ finite}$$$

Lean4

/-- An affine-independent subset of a finite-dimensional affine space is finite. -/
theorem finite_set_of_fin_dim_affineIndependent [FiniteDimensional k V] {s : Set ι} {f : s → P}
    (hi : AffineIndependent k f) : s.Finite :=
  @Set.toFinite _ s (finite_of_fin_dim_affineIndependent k hi)

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