English
Valuation of a sum is at least the minimum of the valuations, with a technical condition.
Русский
Оценка суммы не меньше минимума оценок; при общем случае требуется непустость суммы.
LaTeX
$$min(addValuationDef(x), addValuationDef(y)) \le addValuationDef(x+y)$$
Lean4
theorem map_add (x y : ℚ_[p]) : min (addValuationDef x) (addValuationDef y) ≤ addValuationDef (x + y : ℚ_[p]) :=
by
simp only [addValuationDef]
by_cases hxy : x + y = 0
· rw [hxy, if_pos rfl]
exact le_top
· by_cases hx : x = 0
· rw [hx, if_pos rfl, min_eq_right, zero_add]
exact le_top
· by_cases hy : y = 0
· rw [hy, if_pos rfl, min_eq_left, add_zero]
exact le_top
· rw [if_neg hx, if_neg hy, if_neg hxy, ← WithTop.coe_min, WithTop.coe_le_coe]
exact le_valuation_add hxy
