sound — Mathlib

English

Consistency of the defining equivalence for ValueGroupWithZero.

Русский

Согласованность определения эквивалентности для ValueGroupWithZero.

LaTeX

$$$\operatorname{ValueGroupWithZero.sound} \;: \; \text{(h_1,h_2) satisfy equivalence} \Rightarrow \text{equality of quotients}$$$

Lean4

protected theorem sound {x y : R} {t s : posSubmonoid R} (h₁ : x * s ≤ᵥ y * t) (h₂ : y * t ≤ᵥ x * s) :
    ValueGroupWithZero.mk x t = ValueGroupWithZero.mk y s :=
  Quotient.sound ⟨h₁, h₂⟩

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