linearIndepOn_range_iff — Mathlib

English

For an injective map f, linear independence of g on the range of f is equivalent to independence of g ∘ f.

Русский

Для инъективного отображения f независимость функции g на образе f эквивалентна независимости g ∘ f.

LaTeX

$$$\\\\mathrm{LinearIndepOn}_R g (\\\\operatorname{range} f) \\\\iff \\\\mathrm{LinearIndependent}_R (g \\\\circ f).$$$

Lean4

theorem linearIndepOn_range_iff {ι} {f : ι → ι'} (hf : Injective f) (g : ι' → M) :
    LinearIndepOn R g (range f) ↔ LinearIndependent R (g ∘ f) :=
  Iff.symm <| linearIndependent_equiv' (Equiv.ofInjective f hf) rfl

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