eq_of_comp_right_eq' — Mathlib

English

Let f,g: Y → Z. If the functions X ↦ h ≫ f and X ↦ h ≫ g are equal (for all X and h: X → Y), then f = g.

Русский

Пусть f,g: Y → Z. Если отображения X ↦ h ≫ f и X ↦ h ≫ g совпадают для всех X и h: X → Y, то f = g.

LaTeX

$$$ {f,g:Y\\to Z} \\ (\\forall {X} (h:X\\to Y), h\\circ f = h\\circ g) \\Rightarrow f = g $$$

Lean4

theorem eq_of_comp_right_eq' (f g : Y ⟶ Z) (w : (fun {X} (h : X ⟶ Y) => h ≫ f) = fun {X} (h : X ⟶ Y) => h ≫ g) :
    f = g :=
  eq_of_comp_right_eq @fun X h => by convert congr_fun (congr_fun w X) h

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