linearIndependent_span — Mathlib

English

If LinearIndepOn R (g ∘ f) s holds and f is injective on s, then LinearIndepOn R g (f''s) holds.

Русский

Если линейная независимость на композиции g ∘ f для s, и f инъективна на s, тогда LinearIndepOn R g (f '' s) истинна.

LaTeX

$$LinearIndepOn R g (f '' s)$$

Lean4

theorem linearIndependent_span (hs : LinearIndependent R v) :
    LinearIndependent R (M := span R (range v)) (fun i : ι ↦ ⟨v i, subset_span (mem_range_self i)⟩) :=
  LinearIndependent.of_comp (span R (range v)).subtype hs

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