srel_iff_lt — Mathlib

English

For any x,y in R, x ≤ᵥ y is equivalent to valuation x ≤ valuation y; thus the srel corresponds to the order on Γ.

Русский

Для любых x,y в R, x ≤ᵥ y эквивалентно v(x) ≤ v(y); следовательно, отношение srel совпадает с порядком в Γ.

LaTeX

$$$x \le_{\mathrm{v}} y \iff v(x) \le v(y)$$$

Lean4

theorem _root_.Valuation.Compatible.srel_iff_lt {Γ₀ : Type*} [LinearOrderedCommMonoidWithZero Γ₀] {v : Valuation R Γ₀}
    [v.Compatible] {x y : R} : x <ᵥ y ↔ v x < v y := by
  simp [lt_iff_not_ge, ← Valuation.Compatible.rel_iff_le, srel_iff]

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