ofLE_arrow

Mathlib.CategoryTheory.Subobject.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subobject.ofLE_arrow

English

If X ≤ Y are subobjects of B, then the composite of ofLE X Y h with Y.arrow equals X.arrow.

Русский

Если X ≤ Y, то композиция ofLE X Y h с Y.arrow равна X.arrow.

LaTeX

$$$\\text{ofLE } X Y h \\;\\circ Y.arrow = X.arrow$$$

Lean4

@[reassoc (attr := simp)]
theorem ofLE_arrow {B : C} {X Y : Subobject B} (h : X ≤ Y) : ofLE X Y h ≫ Y.arrow = X.arrow :=
  underlying_arrow _

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

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

Разделы

Аффилиация

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