nnnorm_le_iff — Mathlib

English

For r in NNReal, ∥A∥₊ ≤ r if and only if ∥A_{ij}∥₊ ≤ r for all i,j.

Русский

Для r в NNReal выполняется: ∥A∥₊ ≤ r тогда и только тогда, когда ∥A_{ij}∥₊ ≤ r для всех i,j.

LaTeX

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

Lean4

theorem nnnorm_le_iff {r : ℝ≥0} {A : Matrix m n α} : ‖A‖₊ ≤ r ↔ ∀ i j, ‖A i j‖₊ ≤ r := by
  simp_rw [nnnorm_def, pi_nnnorm_le_iff]

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