comp_apply'

Mathlib.CategoryTheory.ConcreteCategory.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.comp_apply'

← MathLib Explorer

English

If f = g, then for any x we have f x = g x.

Русский

Если f = g, то для любого x имеем f x = g x.

LaTeX

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

Lean4

/-- Variation of `ConcreteCategory.comp_apply` that uses `forget` instead. -/
theorem comp_apply' {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (forget C).map (f ≫ g) x = (forget C).map g ((forget C).map f x) :=
  comp_apply f g x

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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