submatrix_mem_matrix_iff — Mathlib

English

If the rows and columns maps r and c are surjective, then submatrix by r,c preserves membership in S.matrix: M.submatrix r c ∈ S.matrix iff M ∈ S.matrix.

Русский

Если отображения строк и столбцов являются сюръективными, то подматрица по r и c сохраняет принадлежность к S.matrix: M.submatrix r c ∈ S.matrix тогда и только тогда, когда M ∈ S.matrix.

LaTeX

$$hr, hc are surjective implies Iff (M.submatrix r c ∈ S.matrix) (M ∈ S.matrix)$$

Lean4

theorem submatrix_mem_matrix_iff {M : Matrix m n α} {r : l → m} {c : o → n} (hr : Function.Surjective r)
    (hc : Function.Surjective c) : M.submatrix r c ∈ S.matrix ↔ M ∈ S.matrix :=
  ⟨(hr.forall.mpr fun _ => hc.forall.mpr fun _ => · _ _), submatrix_mem_matrix⟩

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