toHom_comp_injective — Mathlib

English

If h is an embedding N ↪[L] P, then the map (M →[L] N) → (M →[L] P) given by f ↦ h.toHom ∘ f is injective.

Русский

Если h — вложение N ↪[L] P, тогда отображение f ↦ h.toHom ∘ f инъективно на множестве функций M →[L] N.

LaTeX

$$$\\text{Injective } (h.toHom.comp)$$$

Lean4

theorem toHom_comp_injective (h : N ↪[L] P) : Function.Injective (h.toHom.comp : (M →[L] N) → (M →[L] P)) :=
  by
  intro f g hfg
  ext x; exact h.injective (DFunLike.congr_fun hfg x)

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