abs_le_right_of_norm — Mathlib

English

For all integers m,n, the absolute value of m is bounded by the norm of the two-dimensional integer vector (n,m); with the standard max-norm, this is |m| ≤ max(|n|,|m|).

Русский

Для любых целых чисел m,n выполняется неравенство |m| ≤ ∥(n,m)∥, где нормa является максимальной нормой в паре целых чисел; то есть |m| ≤ max(|n|,|m|).

LaTeX

$$$\lvert m \rvert \le \| (n,m) \|_\infty = \max\{ |n|, |m| \}$$$

Lean4

theorem abs_le_right_of_norm (m n : ℤ) : |m| ≤ ‖![n, m]‖ :=
  by
  simp only [EisensteinSeries.norm_eq_max_natAbs, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.cons_val_fin_one, Nat.cast_max, le_sup_iff]
  right
  rw [Int.abs_eq_natAbs]
  exact Preorder.le_refl _

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