eq_of_comp_left_eq — Mathlib

English

Let f,g:X→Y. If for every Z and every h:Y→Z we have f ≫ h = g ≫ h, then f = g.

Русский

Пусть f,g: X → Y. Если для каждого Z и каждого h: Y → Z выполняется f ∘ h = g ∘ h, то f = g.

LaTeX

$$$ \\forall {C} [\\text{Category } C] \\ {X,Y} (f,g:X\\to Y), (\\forall Z (h:Y\\to Z), f\\circ h = g\\circ h) \\Rightarrow f = g $$$

Lean4

theorem eq_of_comp_left_eq {f g : X ⟶ Y} (w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h) : f = g := by
  convert w (𝟙 Y) <;> simp

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