liftOn₂_mk — Mathlib

English

The liftOn₂ operation evaluated on mk m s and mk m' s' gives f m s m' s' regardless of chosen witness, i.e. liftOn₂ (mk m s) (mk m' s') f h = f m s m' s'.

Русский

Операция liftOn₂, применённая к mk m s и mk m' s', даёт одинаковый результат: liftOn₂ (mk m s) (mk m' s') f h = f m s m' s'.

LaTeX

$$$\text{liftOn₂} (\text{mk } m s) (\text{mk } m' s') f h = f m s m' s'$$$

Lean4

@[simp]
theorem liftOn₂_mk {α : Type*} (m m' : M) (s s' : ℕ+) (f : M → ℕ+ → M → ℕ+ → α)
    (h : ∀ (m n m' n' : M) (s t s' t' : ℕ+), mk m s = mk m' s' → mk n t = mk n' t' → f m s n t = f m' s' n' t') :
    liftOn₂ (mk m s) (mk m' s') f h = f m s m' s' :=
  rfl

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