cancel_epi — Mathlib

English

Let f:X→Y be an epimorphism. Then f ≫ g = f ≫ h if and only if g = h for any g,h:Y→Z.

Русский

Пусть f:X→Y — эпиморфизм. Тогда f ≫ g = f ≫ h эквивалентно g = h для любых g,h:Y→Z.

LaTeX

$$$ (f:X\\to Y)\\; [\\mathrm{Epi} f]\\; {g,h:Y\\to Z}: (f \\circ g) = (f \\circ h) \\iff g = h $$$

Lean4

theorem cancel_epi (f : X ⟶ Y) [Epi f] {g h : Y ⟶ Z} : f ≫ g = f ≫ h ↔ g = h :=
  ⟨fun p => Epi.left_cancellation g h p, congr_arg _⟩

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