mk_lt_mk — Mathlib

English

For any x, y in R and t, s in posSubmonoid R, the strict order between mk x t and mk y s is equivalent to the strict valuative relation between x s and y t: mk x t < mk y s iff x s <ᵥ y t.

Русский

Для любых x, y ∈ R и t, s ∈ posSubmonoid(R) строгое неравенство mk(x,t) < mk(y,s) эквивалентно строгому valuative-отношению x s <ᵥ y t.

LaTeX

$$$\mathrm{ValueGroupWithZero.mk} \, x \, t < \mathrm{ValueGroupWithZero.mk} \, y \, s \iff x s <_{\mathrm{v}} y t$$$

Lean4

@[simp]
theorem mk_lt_mk (x y : R) (t s : posSubmonoid R) :
    ValueGroupWithZero.mk x t < ValueGroupWithZero.mk y s ↔ x * s <ᵥ y * t := by rw [lt_iff_not_ge, srel_iff, mk_le_mk]

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