norm_le_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem norm_le_iff {r : ℝ} (hr : 0 ≤ r) {A : Matrix m n α} : ‖A‖ ≤ r ↔ ∀ i j, ‖A i j‖ ≤ r := by
  simp_rw [norm_def, pi_norm_le_iff_of_nonneg hr]

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