comp_right_inj — Mathlib

English

For h: M ≃[L] N and f,g: N ≃[L] P, f ∘ h = g ∘ h iff f = g.

Русский

Для h: M ≃_L N и f,g: N ≃_L P, равенство смешанных композиций означает равенство самих функций: f ∘ h = g ∘ h ⇔ f = g.

LaTeX

$$$\bigl(f \circ h = g \circ h\bigr) \iff f = g$$$

Lean4

@[simp]
theorem comp_right_inj (h : M ≃[L] N) (f g : N ≃[L] P) : f.comp h = g.comp h ↔ f = g :=
  ⟨fun eq ↦ h.comp_right_injective eq, congr_arg (fun (r : N ≃[L] P) ↦ r.comp h)⟩

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