nnnorm_lt_iff — Mathlib

English

For r in NNReal with r > 0, ∥A∥₊ < r iff ∥A_{ij}∥₊ < r for all i,j.

Русский

Для r ∈ NNReal, r > 0: ∥A∥₊ < r тогда и только тогда, когда ∥A_{ij}∥₊ < r для всех i,j.

LaTeX

$$$\|A\|_+ < r \;\Longleftrightarrow\; ∀ i,j, \|A_{ij}\|_+ < r.$$$

Lean4

theorem nnnorm_lt_iff {r : ℝ≥0} (hr : 0 < r) {A : Matrix m n α} : ‖A‖₊ < r ↔ ∀ i j, ‖A i j‖₊ < r := by
  simp_rw [nnnorm_def, pi_nnnorm_lt_iff hr]

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