mk_apply

Mathlib.CategoryTheory.Sites.ConcreteSheafification

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Meq.mk_apply

English

If x and x1 are Meq witnesses equal under a condition, their Plus.mk are equal.

Русский

Если x и x1 являются свидетелями Meq, равные при условии, их Plus.mk равны.

LaTeX

$$$Eq (Plus.mk x) (Plus.mk x1)$$$

Lean4

theorem mk_apply {X : C} {P : Cᵒᵖ ⥤ D} (S : J.Cover X) (x : ToType (P.obj (op X))) (I : S.Arrow) :
    mk S x I = P.map I.f.op x :=
  rfl

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

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

Разделы

Аффилиация

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