cancel_mono — Mathlib

English

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

Русский

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

LaTeX

$$$ (g,h: Z\\to X)\\; (g \\circ f) = (h \\circ f) \\iff g = h $$$

Lean4

theorem cancel_mono (f : X ⟶ Y) [Mono f] {g h : Z ⟶ X} : g ≫ f = h ≫ f ↔ g = h :=
  -- Porting note: in Lean 3 we could just write `congr_arg _` here.

  ⟨fun p => Mono.right_cancellation g h p, congr_arg (fun k => k ≫ f)⟩

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