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)