leftUnitor_comp_inv — Mathlib

English

Relation between left whiskering by f and the inverse of left unitor on the composite f ≫ g.

Русский

Связь между левым висением на f и обратным левому уитору на композицию f ≫ g.

LaTeX

$$$ f ◁ (λ_ f)^{-1} = (λ_{f ≫ g})^{-1} ≫ (α_ (𝟙 a) f g)^{hom} $$$

Lean4

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

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