condition

Mathlib.CategoryTheory.Limits.Shapes.Reflexive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.ReflexiveCofork.condition

English

For a Reflexive Cofork G on F, the two legs satisfy F.map left ≫ G.π = F.map right ≫ G.π (same as above).

Русский

Для кофора G над F выполняется равенство F.map left ≫ G.π = F.map right ≫ G.π.

LaTeX

$$$F.map\ left \;\gg\; G.\pi = F.map\ right \;\gg\; G.\pi$$$

Lean4

theorem condition (G : ReflexiveCofork F) : F.map left ≫ G.π = F.map right ≫ G.π := by
  rw [Cocone.w G left, Cocone.w G right]

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

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

Разделы

Аффилиация

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