map_eq_of_sub_lt — Mathlib

English

If v x ≠ v y and v x > v y, then v(x + y) = v x; if v y < v x, then v(x - y) = v y.

Русский

Если v x ≠ v y и v x > v y, тогда v(x+y) = v x; если v y < v x, тогда v(x-y) = v y.

LaTeX

$$$ (h : v x \\neq v y) \\Rightarrow v(x+y) = \\max(v x, v y)$$$

Lean4

theorem map_eq_of_sub_lt (h : v (y - x) < v x) : v y = v x :=
  by
  have := Valuation.map_add_of_distinct_val v (ne_of_gt h).symm
  rw [max_eq_right (le_of_lt h)] at this
  simpa using this

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