map' — Mathlib

English

If hv is LI and f is injective (ker f = ⊥), then f ∘ v is LI.

Русский

Если hv линейно независимо и f вписано инъективно (ker f = ⊥), то f ∘ v линейно независимо.

LaTeX

$$$\\text{LinearIndependent } R\\ v \\rightarrow (\\ker f = \\{0\\})\\rightarrow \\text{LinearIndependent } R (f \\circ v)$$$

Lean4

/-- An injective linear map sends linearly independent families of vectors to linearly independent
families of vectors. See also `LinearIndependent.map` for a more general statement. -/
theorem map' (hv : LinearIndependent R v) (f : M →ₗ[R] M') (hf_inj : LinearMap.ker f = ⊥) :
    LinearIndependent R (f ∘ v) :=
  hv.map <| by simp_rw [hf_inj, disjoint_bot_right]

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