ext_apply

Mathlib.CategoryTheory.ConcreteCategory.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ConcreteCategory.ext_apply

English

If two morphisms act identically on all underlying elements, then they are equal.

Русский

Если два морфизма действуют одинаково на всех базовых элементах, значит они равны.

LaTeX

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

Lean4

theorem ext_apply {X Y : C} {f g : X ⟶ Y} (h : ∀ x, f x = g x) : f = g :=
  ext (DFunLike.ext _ _ h)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru