submatrix — Mathlib

English

Let A be a symmetric matrix. Then for any index map f : M → N, the submatrix of A formed by selecting rows and columns via f is also symmetric.

Русский

Пусть A — симметричная матрица. Тогда для любого отображения индексов f : M → N полученная подматрица A, ограниченная по строкам и столбцам функцией f, тоже симметрична.

LaTeX

$$$\forall A \in M_{n \times n}(\alpha),\ A^{T}=A\ \Rightarrow\ \forall f: M \to N,\ (A_{\;f}^{\;f})^{T}=A_{\;f}^{\;f}$$$

Lean4

@[simp]
theorem submatrix {A : Matrix n n α} (h : A.IsSymm) (f : m → n) : (A.submatrix f f).IsSymm :=
  (transpose_submatrix _ _ _).trans (h.symm ▸ rfl)

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