matrix_strictMono_of_nonempty — Mathlib

English

If the index set n is nonempty, the matrix functor is strictly monotone.

Русский

Если множество индексов n не пусто, отображение по матрицам является строгой монотонной.

LaTeX

$$matrix_strictMono_of_nonempty [Nonempty n] : StrictMono (matrix (R := R) n)$$

Lean4

theorem matrix_strictMono_of_nonempty [Nonempty n] : StrictMono (matrix (R := R) n) :=
  matrix_monotone n |>.strictMono_of_injective <| matrix_injective _

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