lift₂_mk — Mathlib

English

For x,y ∈ R and z,w ∈ posSubmonoid R, lift₂ f hf (mk x z) (mk y w) = f x z y w.

Русский

Для любых x,y ∈ R и z,w ∈ posSubmonoid R выполняется lift₂ f hf (mk x z) (mk y w) = f x z y w.

LaTeX

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

Lean4

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

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