linearIndepOn_iff_of_injOn — Mathlib

English

A protected theorem establishing an equivalence of linear independence under a linear map with a specified injection condition.

Русский

Защищенная теорема устанавливает эквивалентность линейной независимости под линейным отображением при заданном условии инъекции.

LaTeX

$$$\\\\mathrm{LinearIndepOn}_R (f \\circ v) s \\\\iff \\\\mathrm{LinearIndepOn}_R v s,$ при условии $\\\\mathrm{InjOn} (f) (\\\\operatorname{span} R (\\\\operatorname{range} v))$.$$

Lean4

protected theorem linearIndepOn_iff_of_injOn (f : M →ₗ[R] M') (hf_inj : Set.InjOn f (span R (v '' s))) :
    LinearIndepOn R (f ∘ v) s ↔ LinearIndepOn R v s :=
  f.linearIndependent_iff_of_injOn (by rwa [← image_eq_range]) (v := fun i : s ↦ v i)
    -- TODO : Rename this `LinearIndependent.of_subsingleton`.

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