English
For f : α → β → γ, and h compatible with ≈, lift₂ f h applied to (Quotient.mk _ a) and (Quotient.mk _ b) gives f a b.
Русский
Пусть f : α → β → γ, и h совместим с ≈. Применение lift₂ к (Quotient.mk _ a) и (Quotient.mk _ b) даёт f a b.
LaTeX
$$$\\operatorname{Quotient.lift₂} f h (\\operatorname{Quotient.mk} \\_ a) (\\operatorname{Quotient.mk} \\_ b) = f a b$$$
Lean4
@[simp]
theorem lift₂_mk {α : Sort*} {β : Sort*} {γ : Sort*} {_ : Setoid α} {_ : Setoid β} (f : α → β → γ)
(h : ∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), a₁ ≈ b₁ → a₂ ≈ b₂ → f a₁ a₂ = f b₁ b₂) (a : α) (b : β) :
Quotient.lift₂ f h (Quotient.mk _ a) (Quotient.mk _ b) = f a b :=
rfl
