congr_hom — Mathlib

English

If two morphisms f,g in a concrete category are equal, then their actions on all elements are equal.

Русский

Если два морфизма f, g в конкретной категории равны, то они одинаково действуют на все элементы.

LaTeX

$$$h : f = g \Rightarrow \forall x, f x = g x$$$

Lean4

/-- Analogue of `congr_fun h x`,
when `h : f = g` is an equality between morphisms in a concrete category.
-/
theorem congr_hom {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : X) : f x = g x :=
  congrFun (congrArg (fun k : X ⟶ Y => (k : X → Y)) h) x

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