IsEquiv — Mathlib

English

Two valuations v1 and v2 are equivalent if they induce the same preorder on R; i.e., for all r,s, v1(r) ≤ v1(s) iff v2(r) ≤ v2(s).

Русский

Две оценки v1 и v2 эквивалентны, если они порождают одинаковый предордер на R; то есть для любых r,s верно v1(r) ≤ v1(s) эквивалентно v2(r) ≤ v2(s).

LaTeX

$$$\\forall r,s\\, (v_1\\ r \\le v_1\\ s) \\iff (v_2\\ r \\le v_2\\ s)$$$

Lean4

/-- Two valuations on `R` are defined to be equivalent if they induce the same preorder on `R`. -/
def IsEquiv (v₁ : Valuation R Γ₀) (v₂ : Valuation R Γ'₀) : Prop :=
  ∀ r s, v₁ r ≤ v₁ s ↔ v₂ r ≤ v₂ s

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