finrank_vectorSpan_insert_le_set — Mathlib

English

The same bound for finrank holds in the vector-span context when inserting p into an affine subspace s.

Русский

Та же граница по размерности справедлива векторному Span при добавлении p в аффинное подпространство s.

LaTeX

$$finrank_k(vectorSpan_k(insert p ((s: Set P)))) ≤ finrank_k((direction_affineSpan k s)) + 1$$

Lean4

/-- Adding a point to a set with a finite-dimensional span increases the dimension by at most
one. -/
theorem finrank_vectorSpan_insert_le_set (s : Set P) (p : P) :
    finrank k (vectorSpan k (insert p s)) ≤ finrank k (vectorSpan k s) + 1 :=
  by
  rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, direction_affineSpan]
  refine (finrank_vectorSpan_insert_le _ _).trans (add_le_add_right ?_ _)
  rw [direction_affineSpan]

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