isEquiv_iff_val_lt_val — Mathlib

English

If for all x, v x ≤ 1 ⇔ v' x ≤ 1, then v ≈ v'.

Русский

Если для всех x выполняется v(x) ≤ 1 ⇔ v'(x) ≤ 1, тогда v ≈ v'.

LaTeX

$$$ (\forall x, v x \le 1 \iff v' x \le 1) \rightarrow v \IsEquiv v' $$$

Lean4

theorem isEquiv_iff_val_lt_val [LinearOrderedCommMonoidWithZero Γ₀] [LinearOrderedCommMonoidWithZero Γ'₀]
    {v : Valuation K Γ₀} {v' : Valuation K Γ'₀} : v.IsEquiv v' ↔ ∀ {x y : K}, v x < v y ↔ v' x < v' y :=
  by
  simp only [IsEquiv, le_iff_le_iff_lt_iff_lt]
  exact forall_comm

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