w — Mathlib · SciLib

English

Let f : a ⟶ b and g : a ⟶ c, with s,t : RightExtension f g. For any η : s ⟶ t, the left whiskering of η with f together with t.counit equals s.counit; i.e., f ◁ η.left ≫ t.counit = s.counit.

Русский

Пусть f : a ⟶ b, g : a ⟶ c, и s,t — правое расширение (RightExtension) для f,g. Для любого η : s ⟶ t выполняется левое растяжение η слева от f в сочетании со counit t, давая s.counit: f ◁ η.left ≫ t.counit = s.counit.

LaTeX

$$$f \; ◁ \; \eta.left \; ≫ \; t.counit = s.counit$$$

Lean4

@[reassoc (attr := simp)]
theorem w {s t : RightExtension f g} (η : s ⟶ t) : f ◁ η.left ≫ t.counit = s.counit :=
  CostructuredArrow.w η

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