inr

Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.BinaryCofan.inr

English

The second inclusion of a binary cofan.

Русский

Вторая инклюзия двоичной кофана.

LaTeX

$$$$ \text{inr} c = c.\iota(right) $$$$

Lean4

/-- The second inclusion of a binary cofan. -/
abbrev inr {X Y : C} (s : BinaryCofan X Y) :=
  s.ι.app ⟨WalkingPair.right⟩

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

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

Разделы

Аффилиация

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