lift_cRank_submatrix — Mathlib

English

The lifted cardinal rank of a submatrix equals the lifted cardinal rank of the whole matrix: lift(cRank(A_submatrix em en)) = lift(cRank(A)).

Русский

Вознесённый кардинальный ранг подматрицы равен вознесённому ранг-у всей матрицы: lift(cRank(A_submatrix em en)) = lift(cRank(A)).

LaTeX

$$$\operatorname{lift}(cRank(A_{\text{submatrix }(em,en)})) = \operatorname{lift}(cRank(A))$$$

Lean4

@[simp]
theorem lift_cRank_submatrix {n : Type un} (A : Matrix m n R) (em : m₀ ≃ m) (en : n₀ ≃ n) :
    lift.{um} (cRank (A.submatrix em en)) = lift.{um₀} (cRank A) :=
  (A.lift_cRank_submatrix_le em en).antisymm <| by
    simpa using ((A.reindex em.symm en.symm).lift_cRank_submatrix_le em.symm en.symm)

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