congr_hom — Mathlib

English

Let X and Y be objects in a category with a forgetful functor to sets. If f and g are morphisms X → Y and h is the equality f = g, then for every element x of the underlying set of X, f x = g x.

Русский

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

LaTeX

$$$\forall {X Y : C} {f g : X \to Y} (h : f = g), \forall x : (forget\ C).obj X, f\ x = g\ x$$$

Lean4

theorem congr_hom {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : X) : f x = g x :=
  congr_fun (congr_arg (fun f : X ⟶ Y => (f : X → Y)) h) x

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