nnnorm_entry_le_entrywise_sup_nnnorm

Mathlib.Analysis.Matrix

URI: https://scilib.ai/kg/mathlib#Matrix.nnnorm_entry_le_entrywise_sup_nnnorm

← MathLib Explorer

English

For any A and indices i,j, ∥A_{ij}∥₊ ≤ ∥A∥₊.

Русский

Для любых A и индексов i,j: ∥A_{ij}∥₊ ≤ ∥A∥₊.

LaTeX

$$$\|A_{ij}\|_+ \le \|A\|_+.$$$

Lean4

theorem nnnorm_entry_le_entrywise_sup_nnnorm (A : Matrix m n α) {i : m} {j : n} : ‖A i j‖₊ ≤ ‖A‖₊ :=
  (nnnorm_le_pi_nnnorm (A i) j).trans (nnnorm_le_pi_nnnorm A i)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru