isEquiv_iff_val_le_one — Mathlib

English

Two valuations v and v' are equivalent iff for all x, v(x) ≤ 1 iff v'(x) ≤ 1.

Русский

Две оценки эквивалентны тогда и только тогда, когда для каждого x выполняется v(x) ≤ 1 ⇔ v'(x) ≤ 1.

LaTeX

$$$isEquiv(v,v') \\iff \\forall x,\\ v(x) \\le 1 \\iff v'(x) \\le 1.$$$

Lean4

theorem isEquiv_iff_val_le_one [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀]
    {v : Valuation K Γ₀} {v' : Valuation K Γ'₀} : v.IsEquiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1 :=
  ⟨IsEquiv.le_one_iff_le_one, isEquiv_of_val_le_one⟩

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