injective_comp — Mathlib

English

If h: N ≃[L] P, then the map f ↦ f ∘ h: (M ≃[L] N) → (M ≃[L] P) is injective; i.e., f ∘ h = g ∘ h implies f = g.

Русский

Если h: N ≃_L P, то отображение f ↦ f ∘ h: (M ≃_L N) → (M ≃_L P) инъективно; то есть f ∘ h = g ∘ h ⇒ f = g.

LaTeX

$$$\text{Injective}\bigl(f \mapsto f \circ h\bigr)$$$

Lean4

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

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