English
Over a division ring K, for a family v: ι → V and x ∈ V, the linear independence of the function o ↦ Option.casesOn' o x v is equivalent to the conjunction of linear independence of v and x not in span K (range v).
Русский
Имея K-дивизионное кольцо, для семейства v: ι → V и вектора x, линейная независимость функции o ↦ Option.casesOn' o x v эквивалентна сочетанию линейной независимости v и того, что x не лежит в span_K(range v).
LaTeX
$$$\operatorname{LinearIndependent}_K\bigl(o \mapsto o\text{.casesOn'}\ x\ v\bigr) \iff \bigl( \operatorname{LinearIndependent}_K(v) \land x \notin \operatorname{span}_K(\operatorname{range}(v)) \bigr)$$$
Lean4
theorem linearIndependent_option' :
LinearIndependent K (fun o => Option.casesOn' o x v : Option ι → V) ↔
LinearIndependent K v ∧ x ∉ Submodule.span K (range v) :=
by
-- Porting note: Explicit universe level is required in `Equiv.optionEquivSumPUnit`.
rw [← linearIndependent_equiv (Equiv.optionEquivSumPUnit.{u'} ι).symm, linearIndependent_sum, @range_unique _ PUnit,
@linearIndependent_unique_iff PUnit, disjoint_span_singleton]
dsimp [(· ∘ ·)]
refine ⟨fun h => ⟨h.1, fun hx => h.2.1 <| h.2.2 hx⟩, fun h => ⟨h.1, ?_, fun hx => (h.2 hx).elim⟩⟩
rintro rfl
exact h.2 (zero_mem _)
