congr_arg — Mathlib

English

The forgetful map agrees with the canonical hom on the concrete category.

Русский

Забывающий отображение совпадает с каноническим отображением гомоморфизма в конкретной категории.

LaTeX

$$$(forget C).map f = @ConcreteCategory.hom _ _ _ _ _ (HasForget.toConcreteCategory C) _ _ f$$$

Lean4

/-- Analogue of `congr_arg f h`,
when `h : x = x'` is an equality between elements of objects in a concrete category.
-/
protected theorem congr_arg {X Y : C} (f : X ⟶ Y) {x x' : ToType X} (h : x = x') : f x = f x' :=
  congrArg (f : ToType X → ToType Y) h

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