prod_fac₁ — Mathlib

English

Equality of two curried lifted constructs after flips equals the same lifted structure.

Русский

Равенство двух карриованных поднятых конструкторов после разворотов эквивалентно той же поднятой структуре.

LaTeX

$$$W_2.Q \\cdot (\\text{curry.obj } (prodLift F hF))^{\\text{flip}} = (prodLift_1 F hF)^{\\text{flip}}$$$

Lean4

theorem prod_fac₁ [W₂.ContainsIdentities] : W₁.Q ⋙ prodLift₁ F hF = curry.obj F :=
  Construction.fac _ _

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