w — Mathlib · SciLib

English

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

Русский

Пусть f : b ⟶ a, g : c ⟶ a, и s,t — правое поднятие (RightLift) для 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 {s t : RightLift f g} (h : s ⟶ t) : h.left ▷ f ≫ t.counit = s.counit :=
  CostructuredArrow.w h

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