English
Given a function f : R × posSubmonoid R → α and a compatibility condition hf, there is a well-defined lift to ValueGroupWithZero R, i.e., a function lift f hf : ValueGroupWithZero R → α obtained by quotient-lifting of f on representatives.
Русский
Существует корректная подъемная функция для множества значений: если f : R × posSubmonoid R → α и выполняется совместимость hf, тогда можно определить непрерывный перенос на ValueGroupWithZero R.
LaTeX
$$$ \text{ValueGroupWithZero.lift}(f,hf) : \operatorname{ValueGroupWithZero} R \to \alpha \text{ is defined by } \text{Quotient.lift}( (x,y) \mapsto f\,x\,y) \text{ (well-defined by } hf).$$$
Lean4
/-- Lifts a function `R → posSubmonoid R → α` to the value group-with-zero of `R`. -/
protected def lift {α : Sort*} (f : R → posSubmonoid R → α)
(hf : ∀ (x y : R) (t s : posSubmonoid R), x * t ≤ᵥ y * s → y * s ≤ᵥ x * t → f x s = f y t)
(t : ValueGroupWithZero R) : α :=
Quotient.lift (fun (x, y) => f x y) (fun (x, t) (y, s) ⟨h₁, h₂⟩ => hf x y s t h₁ h₂) t
