w — Mathlib · SciLib

English

Let f : a ⟶ b and g : a ⟶ c, and s,t be LeftExtension f g. For any morphism η : s ⟶ t, the unit is preserved under right whiskering: s.unit ≫ f ◁ η.right = t.unit.

Русский

Пусть f : a ⟶ b, g : a ⟶ c, и s,t — левое продолжение (LeftExtension) для f и g. Для любого гомоморфизма η : s ⟶ t выполняется сохранение единичного компонента: s.unit ≫ f ◁ η.right = t.unit.

LaTeX

$$$\forall \eta: s \to t,\; s.unit ≫ f \; ◁ \; \eta.right = t.unit$$$

Lean4

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

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