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_eq_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.eq_one_iff_eq_one]
· intro h
apply isEquiv_of_val_le_one
intro x
constructor
· intro hx
rcases lt_or_eq_of_le hx with hx' | hx'
· have : v (1 + x) = 1 := by
rw [← v.map_one]
apply map_add_eq_of_lt_left
simpa
rw [h] at this
rw [show x = -1 + (1 + x) by simp]
refine le_trans (v'.map_add _ _) ?_
simp [this]
· rw [h] at hx'
exact le_of_eq hx'
· intro hx
rcases lt_or_eq_of_le hx with hx' | hx'
· have : v' (1 + x) = 1 := by
rw [← v'.map_one]
apply map_add_eq_of_lt_left
simpa
rw [← h] at this
rw [show x = -1 + (1 + x) by simp]
refine le_trans (v.map_add _ _) ?_
simp [this]
· rw [← h] at hx'
exact le_of_eq hx'
