linearIndependent_fin_snoc — Mathlib

English

Let v: Fin (n+1) → V. Then v is linearly independent iff its tail is independent and its first element is not in the span of the tail.

Русский

Пусть v: Fin(n+1) → V. Тогда независимость v эквивалентна независимости хвоста и тому, что первый элемент не лежит во span хвоста.

LaTeX

$$$\operatorname{LinearIndependent}_K v \iff \bigl( \operatorname{LinearIndependent}_K(\operatorname{Fin.tail} v) \land v(0) \notin \operatorname{span}_K(\operatorname{range}(\operatorname{Fin.tail} v)) \bigr)$$$

Lean4

theorem linearIndependent_fin_snoc {n} {v : Fin n → V} :
    LinearIndependent K (Fin.snoc v x : Fin (n + 1) → V) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (range v) := by
  rw [Fin.snoc_eq_cons_rotate, ← Function.comp_def, linearIndependent_equiv, linearIndependent_fin_cons]

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