mk_app

Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

URI: https://scilib.ai/kg/mathlib#PresheafOfModules.Derivation'.mk_app

English

The app constructor for Derivation' satisfies that (mk d d_map).app X = d X for any X, i.e., the app construction is compatible with the given family d.

Русский

Конструктор app для Derivation' удовлетворяет (mk d d_map).app X = d X для любого X.

LaTeX

$$$(mk\ d\ d\_map).app\ X = d X$$$

Lean4

@[simp]
theorem mk_app (X : Dᵒᵖ) : (mk d d_map).app X = d X :=
  rfl

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

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

Разделы

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

Аффилиация

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