matrix_strictMono_of_nonempty — Mathlib

English

If the index set n is nonempty, the map I ↦ I.matrix n is strictly increasing: I ⊊ J implies I.matrix n ⊊ J.matrix n.

Русский

Если множество индексов ненулевое, отображение I ↦ I.matrix n strictly возрастает: I ⊊ J ⇒ I.matrix n ⊊ J.matrix n.

LaTeX

$$$$ [\\text{Nonempty } n] \\Rightarrow I \\subset J \\Rightarrow I^{\\mathrm{matrix}}_n \\subset J^{\\mathrm{matrix}}_n \\text{ with strict inclusion.} $$$$

Lean4

theorem matrix_strictMono_of_nonempty [h : Nonempty n] : StrictMono (matrix (R := R) n) :=
  matrix_monotone n |>.strictMono_of_injective <|
    .comp (fun _ _ => mk.inj) <| (RingCon.matrix_injective n).comp ringCon_injective

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