English
The infinity valuation satisfies the nonarchimedean inequality: v(x+y) ≤ max(v(x), v(y)).
Русский
Валюация на бесконечности удовлетворяет неархимедову неравенство: v(x+y) ≤ max(v(x), v(y)).
LaTeX
$$$\infty\text{-Valuation}(x+y) \le \max\{\infty\text{-Valuation}(x), \infty\text{-Valuation}(y)\}$$$
Lean4
theorem map_add_le_max' (x y : RatFunc Fq) :
inftyValuationDef Fq (x + y) ≤ max (inftyValuationDef Fq x) (inftyValuationDef Fq y) :=
by
by_cases hx : x = 0
· rw [hx, zero_add]
conv_rhs => rw [inftyValuationDef, if_pos (Eq.refl _)]
rw [max_eq_right (WithZero.zero_le (inftyValuationDef Fq y))]
· by_cases hy : y = 0
· rw [hy, add_zero]
conv_rhs => rw [max_comm, inftyValuationDef, if_pos (Eq.refl _)]
rw [max_eq_right (WithZero.zero_le (inftyValuationDef Fq x))]
· by_cases hxy : x + y = 0
· rw [inftyValuationDef, if_pos hxy]; exact zero_le'
· rw [inftyValuationDef, inftyValuationDef, inftyValuationDef, if_neg hx, if_neg hy, if_neg hxy]
simpa using RatFunc.intDegree_add_le hy hxy
