comp_of_image — Mathlib

English

If h is LinearIndepOn over R for v on s, and f is injective on s, then composing v with f preserves linear independence: LinearIndepOn R (f ∘ v) s.

Русский

Если v линейно независим над R на s, и f инъективна на s, то композиция f ∘ v сохраняет линейную независимость на s.

LaTeX

$$LinearIndepOn R (f ∘ v) s$$

Lean4

theorem comp_of_image {s : Set ι'} {f : ι' → ι} (h : LinearIndepOn R v (f '' s)) (hf : InjOn f s) :
    LinearIndepOn R (v ∘ f) s :=
  LinearIndependent.comp h _ (Equiv.Set.imageOfInjOn _ _ hf).injective

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