English
The p-adic norm satisfies the triangle inequality: padicNorm p (q + r) ≤ padicNorm p q + padicNorm p r.
Русский
Норма p-адическая удовлетворяет неравенство треугольника: padicNorm p (q + r) ≤ padicNorm p q + padicNorm p r.
LaTeX
$$$ padicNorm\ p\ (q + r) \leq padicNorm\ p\ q + padicNorm\ p\ r $$$
Lean4
/-- The `p`-adic norm respects the triangle inequality: the norm of `p + q` is at most the norm of
`p` plus the norm of `q`. -/
theorem triangle_ineq (q r : ℚ) : padicNorm p (q + r) ≤ padicNorm p q + padicNorm p r :=
calc
padicNorm p (q + r) ≤ max (padicNorm p q) (padicNorm p r) := padicNorm.nonarchimedean
_ ≤ padicNorm p q + padicNorm p r := max_le_add_of_nonneg (padicNorm.nonneg _) (padicNorm.nonneg _)
