map_f₃₄_op_glue

Mathlib.CategoryTheory.Sites.MayerVietorisSquare

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.map_f₃₄_op_glue

English

Similarly, P.map S.f₃₄.op (h.glue u v huv) = v.

Русский

Аналогично, P.map f34.op (glue) = v.

LaTeX

$$P.map S.f₃₄.op (h.glue u v huv) = v$$

Lean4

@[simp]
theorem map_f₃₄_op_glue : P.map S.f₃₄.op (h.glue u v huv) = v :=
  PullbackCone.IsLimit.equivPullbackObj_symm_apply_snd h.isLimit _

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

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

Разделы

Аффилиация

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