English
Lift₂ lifts a binary function f: M → M → α to MulArchimedeanClass M → MulArchimedeanClass M → α, respecting mk-equivalence in both arguments.
Русский
Lift₂ поднимает бинарную функцию f: M → M → α до MulArchimedeanClass M → MulArchimedeanClass M → α, учитывая эквивалентность по mk в обеих аргументах.
LaTeX
$$$lift₂: (M \to M \to α) \to (∀ a₁ b₁ a₂ b₂, mk a₁ = mk b₁ → mk a₂ = mk b₂ → f a₁ a₂ = f b₁ b₂) \to MulArchimedeanClass M → MulArchimedeanClass M → α$$$
Lean4
/-- Lift a `M → M → α` function to `MulArchimedeanClass M → MulArchimedeanClass M → α`. -/
@[to_additive /-- Lift a `M → M → α` function to `ArchimedeanClass M → ArchimedeanClass M → α`. -/
]
def lift₂ {α : Type*} (f : M → M → α) (h : ∀ a₁ b₁ a₂ b₂, mk a₁ = mk b₁ → mk a₂ = mk b₂ → f a₁ a₂ = f b₁ b₂) :
MulArchimedeanClass M → MulArchimedeanClass M → α :=
Quotient.lift₂ f fun _ _ _ _ h₁ h₂ ↦ h _ _ _ _ (mk_eq_mk.mpr h₁) (mk_eq_mk.mpr h₂)
