option — Mathlib

English

If v is linearly independent and x is not in span of range v, then the function o ↦ o.casesOn' x v is linearly independent.

Русский

Если v линейно независимо и x не лежит в span(range v), то функция o ↦ o.casesOn' x v линейно независима.

LaTeX

$$$\operatorname{LinearIndependent}_K(v) \land x \notin \operatorname{span}_K(\operatorname{range}(v)) \Rightarrow \operatorname{LinearIndependent}_K\bigl(o \mapsto o\text{.casesOn'}\ x\ v\bigr)$$$

Lean4

theorem option (hv : LinearIndependent K v) (hx : x ∉ Submodule.span K (range v)) :
    LinearIndependent K (fun o => Option.casesOn' o x v : Option ι → V) :=
  linearIndependent_option'.2 ⟨hv, hx⟩

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