English
The equivalence relation used to form the value group with zero is defined on R × posSubmonoid R by (x,s) ~ (y,t) iff x t ≤ᵥ y s and y s ≤ᵥ x t, and it is an equivalence relation extending refl, symmetry, transitivity.
Русский
Эквивалентность на R × posSubmonoid R задаётся так: (x,s) ≈ (y,t) тогда и только тогда, когда x t ≤ᵥ y s и y s ≤ᵥ x t; это Relation; она эквивалентна по refl, symmetry, trans.
LaTeX
$$$\text{valueSetoid }(R) :\,\text{Setoid}(R \times \operatorname{posSubmonoid}R)$ with $ (x,s) \sim (y,t) \iff x t ≤ᵥ y s ∧ y s ≤ᵥ x t $$$
Lean4
/-- The setoid used to construct `ValueGroupWithZero R`. -/
def valueSetoid : Setoid (R × posSubmonoid R)
where
r := fun (x, s) (y, t) => x * t ≤ᵥ y * s ∧ y * s ≤ᵥ x * t
iseqv :=
{ refl ru := ⟨rel_refl _, rel_refl _⟩
symm h := ⟨h.2, h.1⟩
trans := by
rintro ⟨r, u⟩ ⟨s, v⟩ ⟨t, w⟩ ⟨h1, h2⟩ ⟨h3, h4⟩
constructor
· have := rel_mul h1 (rel_refl ↑w)
rw [mul_right_comm s] at this
have := rel_trans this (rel_mul h3 (rel_refl _))
rw [mul_right_comm r, mul_right_comm t] at this
simpa using this
· have := rel_mul h4 (rel_refl ↑u)
rw [mul_right_comm s] at this
have := rel_trans this (rel_mul h2 (rel_refl _))
rw [mul_right_comm t, mul_right_comm r] at this
simpa using this }
