English
For f and h as above, liftOn₂ (Quotient.mk ...) equals f on representatives: liftOn₂ (Quotient.mk a) (Quotient.mk b) f h = f a b.
Русский
При тех же условиях liftOn₂ (Quotient.mk ...) на представителях равняется f на представителях: liftOn₂ (Quotient.mk a) (Quotient.mk b) f h = f a b.
LaTeX
$$$\\operatorname{Quotient.liftOn₂} (\\operatorname{Quotient.mk} a) (\\operatorname{Quotient.mk} b) f h = f a b$$$
Lean4
@[simp]
theorem liftOn₂_mk {α : Sort*} {β : Sort*} {γ : Sort*} {_ : Setoid α} {_ : Setoid β} (f : α → β → γ)
(h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) (x : α) (y : β) :
Quotient.liftOn₂ (Quotient.mk _ x) (Quotient.mk _ y) f h = f x y :=
rfl
