eq_of_comp_left_eq' — Mathlib

English

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

Русский

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

LaTeX

$$$ {f,g:X\\to Y} \\ Leftarrow (\\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 : (fun {Z} (h : Y ⟶ Z) => f ≫ h) = fun {Z} (h : Y ⟶ Z) => g ≫ h) : f = g :=
  eq_of_comp_left_eq @fun Z h => by convert congr_fun (congr_fun w Z) h

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