submatrix_mem_matrix — Mathlib

English

If M has all its entries in S, then any submatrix of M also has all entries in S.

Русский

Если все элементы матрицы M принадлежат S, то любая подматрица M также имеет элементы в S.

LaTeX

$$$M \\in S.matrix \\Rightarrow M^{\\text{submatrix}} r c \\in S.matrix$$$

Lean4

theorem submatrix_mem_matrix {M : Matrix m n α} {r : l → m} {c : o → n} (hM : M ∈ S.matrix) :
    M.submatrix r c ∈ S.matrix := by simp_all [Set.mem_matrix]

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