norm_add_eq_max_of_ne — Mathlib

English

If two norms are distinct, the norm of their sum attains the maximum: if ||q|| ≠ ||r|| then ||q + r|| = max(||q||, ||r||).

Русский

Если две нормы различны, то ||q + r|| достигает максимального значения: если ||q|| ≠ ||r||, то ||q + r|| = max(||q||, ||r||).

LaTeX

$$$$\|q + r\| = \max\{\|q\|, \|r\|\} \quad\text{если } \|q\| \neq \|r\|.$$$$

Lean4

theorem norm_add_eq_max_of_ne {q r : ℤ_[p]} : ‖q‖ ≠ ‖r‖ → ‖q + r‖ = max ‖q‖ ‖r‖ :=
  Padic.add_eq_max_of_ne

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