lift₂_mk — Mathlib

English

lift₂_eq_1 states that applying lift₂ to representatives yields the same result as f on those representatives: lift₂ f h (mk a) (mk b) = f a b.

Русский

lift₂_eq_1 утверждает, что применение lift₂ к представителям даёт ту же величину, что и f на самих представителях: lift₂ f h (mk a) (mk b) = f a b.

LaTeX

$$$lift₂ f h (mk a) (mk b) = f a b$$$

Lean4

@[to_additive (attr := simp)]
theorem lift₂_mk {α : Type*} (f : M → M → α) (h : ∀ a₁ b₁ a₂ b₂, mk a₁ = mk b₁ → mk a₂ = mk b₂ → f a₁ a₂ = f b₁ b₂)
    (a b : M) : lift₂ f h (mk a) (mk b) = f a b := by
  unfold lift₂
  exact Quotient.lift₂_mk f (fun _ _ _ _ h₁ h₂ ↦ h _ _ _ _ (mk_eq_mk.mpr h₁) (mk_eq_mk.mpr h₂)) a b

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