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)