sub — Mathlib

English

The p-adic norm of a difference is at most the max of the norms: padicNorm p (q - r) ≤ max(padicNorm p q, padicNorm p r).

Русский

Норма разности не превышает максимум норм: padicNorm p (q − r) ≤ max(padicNorm p q, padicNorm p r).

LaTeX

$$$ padicNorm\ p\ (q - r) \leq \max( padicNorm\ p\ q, padicNorm\ p\ r ) $$$

Lean4

/-- The `p`-adic norm of a difference is at most the max of each component. Restates the archimedean
property of the `p`-adic norm. -/
protected theorem sub {q r : ℚ} : padicNorm p (q - r) ≤ max (padicNorm p q) (padicNorm p r) :=
  by
  rw [sub_eq_add_neg, ← padicNorm.neg r]
  exact padicNorm.nonarchimedean

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