range_mapIncl_mono — Mathlib

English

If there exist linear maps a,b,c,d with range a ≤ range b and range c ≤ range d, then range (map a c) ≤ range (map b d).

Русский

Если существуют линейные отображения a,b,c,d с образами, удовлетворяющими range a ≤ range b и range c ≤ range d, то range (map a c) ≤ range (map b d).

LaTeX

$$$\\operatorname{range}(a) \\leq \\operatorname{range}(b) \\Rightarrow \\operatorname{range}(c) \\leq \\operatorname{range}(d) \\Rightarrow \\operatorname{range}(\\operatorname{map} a c) \\leq \\operatorname{range}(\\operatorname{map} b d)$$$

Lean4

theorem range_mapIncl_mono {p p' : Submodule R P} {q q' : Submodule R Q} (hp : p ≤ p') (hq : q ≤ q') :
    LinearMap.range (mapIncl p q) ≤ LinearMap.range (mapIncl p' q') :=
  range_map_mono (by simpa) (by simpa)

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