linearIndepOn_equiv — Mathlib

English

Linear independence on s is equivalent to linear independence on the image of s under an equivalence of index types.

Русский

Линейная независимость на s эквивалентна независимости на образе s под эквивалентностью индексов.

LaTeX

$$$\\\\mathrm{LinearIndepOn}_R (f \\circ e) s \\\\iff \\\\mathrm{LinearIndepOn}_R f (e '' s),$ где $e$ — эквиваленция.$$

Lean4

theorem linearIndepOn_equiv (e : ι ≃ ι') {f : ι' → M} {s : Set ι} :
    LinearIndepOn R (f ∘ e) s ↔ LinearIndepOn R f (e '' s) :=
  linearIndependent_equiv' (e.image s) <| by simp [funext_iff]

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