prod_fac₂ — Mathlib

English

The product fac equality expresses that the composite of prodLift with projections equals the original F.

Русский

Соотношение fac для произведения выражает равенство композиции prodLift с проекциями и исходной F.

LaTeX

$$$(W_1.Q.prod W_2.Q) \\cdot \\text{prodLift } F hF = F$$$

Lean4

theorem prod_fac₂ : W₂.Q ⋙ (curry.obj (prodLift F hF)).flip = (prodLift₁ F hF).flip :=
  by
  simp only [prodLift, Functor.curry_obj_uncurry_obj, Functor.flip_flip]
  apply Construction.fac

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