posSemidef_submatrix_equiv — Mathlib

English

If a matrix M is PSD, then any relabeled version by a bijection e: m ≃ n, namely M.submatrix e e, is PSD, and conversely.

Русский

Если матрица M является PSD, то любая перестановочная подпроекция по биекции e: m ≃ n, т.е. M.submatrix e e, также PSD, и наоборот.

LaTeX

$$$(M)_{e,e} \text{ PSD } \iff M \text{ PSD}$$$

Lean4

@[simp]
theorem posSemidef_submatrix_equiv {M : Matrix n n R} (e : m ≃ n) : (M.submatrix e e).PosSemidef ↔ M.PosSemidef :=
  ⟨fun h => by simpa using h.submatrix e.symm, fun h => h.submatrix _⟩

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