leftUnitor_inv_left_snd — Mathlib

English

As before, the left unitor maps the unit object to the left factor via fst, reflecting the unit law for the tensor product.

Русский

Левый унитор отображает единичный объект к левому фактору через fst и выражает тензорную единичную законность.

LaTeX

$$$ (\\lambda_Y).inv.left \\circ \\mathrm{fst}(\\mathrm{id}_X) = \\mathrm{id}_{Y.left} $$$

Lean4

@[reassoc (attr := simp)]
theorem leftUnitor_inv_left_snd (Y : Over X) : (λ_ Y).inv.left ≫ pullback.snd (𝟙 X) _ = 𝟙 Y.left :=
  limit.lift_π _ _

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