comp_right_injective — Mathlib

English

If h: N ≃[L] P, then the map f ↦ f ∘ h from (N ≃[L] P) to (M ≃[L] P) is injective.

Русский

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

LaTeX

$$$\operatorname{Injective}\bigl(\lambda f:\nrightarrow [L] P.\; f\circ h\bigr)$$$

Lean4

theorem comp_right_injective (h : M ≃[L] N) : Function.Injective (fun f ↦ f.comp h : (N ≃[L] P) → (M ≃[L] P)) :=
  by
  intro f g hfg
  convert (congr_arg (fun r : (M ≃[L] P) ↦ r.comp h.symm) hfg) <;> rw [comp_assoc, self_comp_symm, comp_refl]

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