English
Two valuations v and v' are equivalent iff for every x, v(x) < 1 iff v'(x) < 1.
Русский
Две оценки эквивалентны тогда и только тогда, когда для каждого x выполняется v(x) < 1 ⇔ v'(x) < 1.
LaTeX
$$$v \\text{ IsEquiv } v' \\iff \\forall x,\\ v(x) < 1 \\iff v'(x) < 1.$$$
Lean4
theorem isEquiv_iff_val_lt_one [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀]
{v : Valuation K Γ₀} {v' : Valuation K Γ'₀} : v.IsEquiv v' ↔ ∀ {x : K}, v x < 1 ↔ v' x < 1 :=
by
constructor
· intro h x
rw [h.lt_one_iff_lt_one]
· rw [isEquiv_iff_val_eq_one]
intro h x
by_cases hx : x = 0
· simp only [(zero_iff _).2 hx, zero_ne_one]
constructor
· intro hh
by_contra h_1
cases ne_iff_lt_or_gt.1 h_1 with
| inl h_2 => simpa [hh, lt_self_iff_false] using h.2 h_2
| inr h_2 =>
rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh
exact hh.not_lt (h.2 ((one_lt_val_iff v' hx).1 h_2))
· intro hh
by_contra h_1
cases ne_iff_lt_or_gt.1 h_1 with
| inl h_2 => simpa [hh, lt_self_iff_false] using h.1 h_2
| inr h_2 =>
rw [← inv_one, ← inv_eq_iff_eq_inv, ← map_inv₀] at hh
exact hh.not_lt (h.1 ((one_lt_val_iff v hx).1 h_2))
