linearIndependent_equiv' — Mathlib

English

If two indexings are related by a bijection, independence is preserved with a corresponding reindexing of the vector map.

Русский

Если две индексации связаны биекцией, независимость сохраняется при соответствующей переразметке отображения векторов.

LaTeX

$$$\\\\mathrm{linearIndependent}_{R} (f \\circ e) \\\\iff \\\\mathrm{linearIndependent}_{R} f,$ где $e$ — биекция между индексами.$$

Lean4

theorem linearIndependent_equiv' (e : ι ≃ ι') {f : ι' → M} {g : ι → M} (h : f ∘ e = g) :
    LinearIndependent R g ↔ LinearIndependent R f :=
  h ▸ linearIndependent_equiv e

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