comp_injective — Mathlib

English

If h is an embedding N ↪[L] P, then composing on the right with h yields an injective map on embeddings: h.comp : (M ↪[L] N) → (M ↪[L] P) is injective.

Русский

Если h — вложение N ↪[L] P, то композиция справа с h даёт инъективное отображение: h.comp : (M ↪[L] N) → (M ↪[L] P) инъективно.

LaTeX

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

Lean4

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

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