map_injOn — Mathlib

English

If w is equal to v on the index set s, then linear independence of v on s is equivalent to the linear independence of w on s.

Русский

Если w совпадает с v на множества индексов s, то линейная независимость v на s эквивалентна линейной независимости w на s.

LaTeX

$$LinearIndepOn R v s ↔ LinearIndepOn R w s when v ≡ w on s$$

Lean4

theorem map_injOn (hv : LinearIndepOn R v s) (f : M →ₗ[R] M') (hf_inj : Set.InjOn f (span R (v '' s))) :
    LinearIndepOn R (f ∘ v) s :=
  (f.linearIndepOn_iff_of_injOn hf_inj).mpr hv

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