norm_entry_le_entrywise_sup_norm

Mathlib.Analysis.Matrix

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

← MathLib Explorer

English

For any A and indices i,j, the entry satisfies ∥A_{ij}∥ ≤ ∥A∥.

Русский

Для любых A и индексов i,j элемент удовлетворяет ∥A_{ij}∥ ≤ ∥A∥.

LaTeX

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

Lean4

theorem norm_entry_le_entrywise_sup_norm (A : Matrix m n α) {i : m} {j : n} : ‖A i j‖ ≤ ‖A‖ :=
  (norm_le_pi_norm (A i) j).trans (norm_le_pi_norm A i)

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

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

Разделы

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

Аффилиация

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