lift_mk — Mathlib

English

For any x ∈ R and y ∈ posSubmonoid R, the lift respects representatives: lift f hf (mk x y) = f x y.

Русский

Для любых x ∈ R и y ∈ posSubmonoid R отображение lift f hf сохраняет представителя: lift f hf (mk x y) = f x y.

LaTeX

$$$ \text{ValueGroupWithZero.lift}(f,hf)(\operatorname{mk} x y) = f x y$$$

Lean4

@[simp]
protected theorem lift_mk {α : 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) (x : R)
    (y : posSubmonoid R) : ValueGroupWithZero.lift f hf (.mk x y) = f x y :=
  rfl

Похожие утверждения