English
Extends lifting to a function f : R × posSubmonoid R × R × posSubmonoid R → α with a two-layer compatibility hf, producing a lift₂ : ValueGroupWithZero R → α applicable to two inputs t₁, t₂.
Русский
Расширение подъёма до функции с двумя входами, обеспечивающей перенос на ValueGroupWithZero R с учётом совместимости hf.
LaTeX
$$$ {\alpha} := \text{Sort*};\ (f : R \to (posSubmonoid R) \to R \to (posSubmonoid R) \to \alpha) \to \\ (\forall x y z w:\; R, \forall t s u v:\; posSubmonoid R, \text{compatibility } hf) \Rightarrow \text{ValueGroupWithZero.lift₂}(f,hf)(t_1)(t_2) : \alpha$$$
Lean4
/-- Lifts a function `R → posSubmonoid R → R → posSubmonoid R → α` to
the value group-with-zero of `R`. -/
protected def lift₂ {α : Sort*} (f : R → posSubmonoid R → R → posSubmonoid R → α)
(hf :
∀ (x y z w : R) (t s u v : posSubmonoid R),
x * t ≤ᵥ y * s → y * s ≤ᵥ x * t → z * u ≤ᵥ w * v → w * v ≤ᵥ z * u → f x s z v = f y t w u)
(t₁ : ValueGroupWithZero R) (t₂ : ValueGroupWithZero R) : α :=
Quotient.lift₂ (fun (x, t) (y, s) => f x t y s)
(fun (x, t) (z, v) (y, s) (w, u) ⟨h₁, h₂⟩ ⟨h₃, h₄⟩ => hf x y z w s t u v h₁ h₂ h₃ h₄) t₁ t₂
