linearIndependent_option — Mathlib

English

For v: ι → V, the independence on insert a s is equivalent to independence on s together with the condition that f a does not lie in the span of f s.

Русский

Для v: ι → V независимость на наборе insert a s эквивалентна независимости на s и условию, что f a не лежит в span(f s).

LaTeX

$$$\text{LinearIndepOn}_K(v,\operatorname{insert} a\,s) \iff \text{LinearIndepOn}_K(v,s) \land (v a \in \operatorname{span}_K(v''s) \to v a \notin \operatorname{span}_K(v''s))$$$

Lean4

theorem linearIndependent_option {v : Option ι → V} :
    LinearIndependent K v ↔
      LinearIndependent K (v ∘ (↑) : ι → V) ∧ v none ∉ Submodule.span K (range (v ∘ (↑) : ι → V)) :=
  by simp only [← linearIndependent_option', Option.casesOn'_none_coe]

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