w — Mathlib · SciLib

English

Let f : b ⟶ a and g : c ⟶ a, with s,t : LeftLift f g. For any h : s ⟶ t, we have h.left ▷ f ≫ t.counit = s.counit; i.e., counits are preserved under left whiskering.

Русский

Пусть f : b ⟶ a, g : c ⟶ a, и s,t — левое поднятие (LeftLift) для f,g. Для любого h : s ⟶ t выполняется h.left ▷ f ≫ t.counit = s.counit; с сохранением counit под левым взведением.

LaTeX

$$$h.left \; \triangleright \; f \; ≫ \; t.counit = s.counit$$$

Lean4

@[reassoc (attr := simp)]
theorem w (h : s ⟶ t) : s.unit ≫ h.right ▷ f = t.unit :=
  StructuredArrow.w h

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