English
For valuations v on K and v′ on K, the following six conditions are pairwise equivalent: (1) v is equivalent to v′; (2) for all x,y in K, v x < v y iff v′ x < v′ y; (3) for all x in K, v x ≤ 1 iff v′ x ≤ 1; (4) for all x in K, v x = 1 iff v′ x = 1; (5) for all x in K, v x < 1 iff v′ x < 1; (6) for all x in K, v(x−1) < 1 iff v′(x−1) < 1.
Русский
Для оцениваний v на K и v′ на K выполняются взаимно эквивалентно шесть условий: (1) v эквивалентно v′; (2) для всех x,y ∈ K выполняется v x < v y ⇔ v′ x < v′ y; (3) для всех x ∈ K v x ≤ 1 ⇔ v′ x ≤ 1; (4) для всех x ∈ K v x = 1 ⇔ v′ x = 1; (5) для всех x ∈ K v x < 1 ⇔ v′ x < 1; (6) для всех x ∈ K v(x−1) < 1 ⇔ v′(x−1) < 1.
LaTeX
$$[(v IsEquiv v') \and for all x,y, v x < v y \iff v' x < v' y \and for all x, v x ≤ 1 \iff v' x ≤ 1 \and for all x, v x = 1 \iff v' x = 1 \and for all x, v x < 1 \iff v' x < 1 \and for all x, v(x-1) < 1 \iff v'(x-1) < 1].TFAE$$
Lean4
theorem isEquiv_tfae [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀)
(v' : Valuation K Γ'₀) :
[v.IsEquiv v', ∀ {x y}, v x < v y ↔ v' x < v' y, ∀ {x}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x}, v x = 1 ↔ v' x = 1,
∀ {x}, v x < 1 ↔ v' x < 1, ∀ {x}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE :=
by
tfae_have 1 ↔ 2 := isEquiv_iff_val_lt_val
tfae_have 1 ↔ 3 := isEquiv_iff_val_le_one
tfae_have 1 ↔ 4 := isEquiv_iff_val_eq_one
tfae_have 1 ↔ 5 := isEquiv_iff_val_lt_one
tfae_have 1 ↔ 6 := isEquiv_iff_val_sub_one_lt_one
tfae_finish
