le_iff — Mathlib

English

For any matrices A,B over 𝕜, A ≤ B if and only if (B − A) is PosSemidef; the relation is exactly the defined preorder.

Русский

Для матриц A,B над 𝕜 верно: A ≤ B if and only if B − A является PosSemidef; отношение совпадает с заданным пред-порядком.

LaTeX

$$$ A \\le B \\;\\Leftrightarrow\\; (B - A).PosSemidef $$$

Lean4

theorem le_iff {A B : Matrix n n 𝕜} : A ≤ B ↔ (B - A).PosSemidef :=
  Iff.rfl

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