submatrix_submatrix — Mathlib

English

Applying a submatrix operation twice is the same as applying a single submatrix with the composed row and column maps: (A.submatrix r1 c1).submatrix r2 c2 = A.submatrix (r1 ∘ r2) (c1 ∘ c2).

Русский

Повторное применение подматрицы эквивалентно одному подмножество через композицию индексов: (A.submatrix r1 c1).submatrix r2 c2 = A.submatrix (r1 ∘ r2) (c1 ∘ c2).

LaTeX

$$$ (A.submatrix\ r_1\ c_1).submatrix\ r_2\ c_2 = A.submatrix (r_1 \circ r_2) (c_1 \circ c_2) $$$

Lean4

@[simp]
theorem submatrix_submatrix {l₂ o₂ : Type*} (A : Matrix m n α) (r₁ : l → m) (c₁ : o → n) (r₂ : l₂ → l) (c₂ : o₂ → o) :
    (A.submatrix r₁ c₁).submatrix r₂ c₂ = A.submatrix (r₁ ∘ r₂) (c₁ ∘ c₂) :=
  ext fun _ _ => rfl

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