nonneg_iff_posSemidef

Mathlib.Analysis.Matrix.Order

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

English

A matrix A is nonnegative in the Loewner order (0 ≤ A) if and only if A is PosSemidef.

Русский

Матрица A неотрицательна в порядке Лоэва, если и только если APosSemidef.

LaTeX

$$$ 0 \\le A \\;\\Leftrightarrow\\; A.PosSemidef $$$

Lean4

theorem nonneg_iff_posSemidef {A : Matrix n n 𝕜} : 0 ≤ A ↔ A.PosSemidef := by rw [le_iff, sub_zero]

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

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

Разделы

Аффилиация

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