injective_compr₂_of_injective — Mathlib

English

If f and g are injective linear maps, then their composed bilinear map f.compr₂ g is injective.

Русский

Если f и g инъективны как линейные отображения, то композиция bilinear f.compr₂ g также инъективна.

LaTeX

$$$\text{Injective}(f) \land \text{Injective}(g) \implies \text{Injective}(f.compr₂ g).$$$

Lean4

/-- A version of `Function.Injective.comp` for composition of a bilinear map with a linear map. -/
theorem injective_compr₂_of_injective (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ) (g : Pₗ →ₗ[R] Qₗ) (hf : Injective f)
    (hg : Injective g) : Injective (f.compr₂ g) :=
  hg.injective_linearMapComp_left.comp hf

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