eRank_submatrix_le — Mathlib

English

The eRank of a submatrix is not greater than the eRank of the original matrix.

Русский

eRank подматрицы не превосходит eRank исходной матрицы.

LaTeX

$$$\operatorname{eRank}(A_{r,c}) \le \operatorname{eRank}(A).$$$

Lean4

theorem eRank_submatrix_le (A : Matrix m n R) (r : m₀ → m) (c : n₀ → n) : (A.submatrix r c).eRank ≤ A.eRank := by
  simpa using OrderHom.mono (β := ℕ∞) Cardinal.toENat <| lift_cRank_submatrix_le A r c

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