liftOn₂_mk — Mathlib

English

For any p, the equality holds: lifting of two mk-arguments yields the same value when evaluated at a and c.

Русский

Для любых двух аргументов mkp равенство сохраняется при подъёме двух аргументов mk.

LaTeX

$$$\text{liftOn₂ } (mk\ a b) (mk\ c d) f H = f a b c d.$$$

Lean4

@[to_additive]
theorem liftOn₂_mk {p : Sort*} (f : M → S → M → S → p) (H) (a c : M) (b d : S) :
    liftOn₂ (mk a b) (mk c d) f H = f a b c d :=
  rfl

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