leftUnitor_comp — Mathlib

English

The left unitor of a composite factors through the left unitor of the first factor and the associator with the identity on the left.

Русский

Левый уитор композиции разлагается через левый уитор первого фактора и ассоциатор с идентичностью слева.

LaTeX

$$$ (\\lambda_{f g})^{inv} = (\\lambda_f)^{inv} \\triangleright g ≫ (α_{\\mathbf{1}_a} f g)^{hom} $$$

Lean4

@[reassoc]
theorem leftUnitor_comp (f : a ⟶ b) (g : b ⟶ c) : (λ_ (f ≫ g)).hom = (α_ (𝟙 a) f g).inv ≫ (λ_ f).hom ▷ g := by simp

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