over_right

Mathlib.CategoryTheory.Comma.Over.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Over.over_right

English

For any object U in Over X, the right component is the unit object (terminal).

Русский

Для любого объекта U в Over(X) правый компонент равен единице (терминальному объекту).

LaTeX

$$$\\forall U:\\mathrm{Over}(X),\\; U.\\text{right} \\cong 1$$$

Lean4

@[simp]
theorem over_right (U : Over X) : U.right = ⟨⟨⟩⟩ := by simp only

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

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

Разделы

Аффилиация

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