English
If the image of a linear map a is contained in the image of b, and the image of c is contained in the image of d, then the image of the product map map a c is contained in the image of map b d.
Русский
Если образ отображения a принадлежит образу b, и образ отображения c принадлежит образу d, то образ отображения map a c принадлежит образу map b d.
LaTeX
$$$\\operatorname{range}(a) \\leq \\operatorname{range}(b),\\; \\operatorname{range}(c) \\leq \\operatorname{range}(d) \\;\Rightarrow\\; \\operatorname{range}(\\operatorname{map} a c) \\leq \\operatorname{range}(\\operatorname{map} b d)$$$
Lean4
theorem range_map_mono [Module R M₂] [Module R M₃] [Module R N₂] [Module R N₃] {a : M →ₗ[R] M₂} {b : M₃ →ₗ[R] M₂}
{c : N →ₗ[R] N₂} {d : N₃ →ₗ[R] N₂} (hab : range a ≤ range b) (hcd : range c ≤ range d) :
range (map a c) ≤ range (map b d) := by
simp_rw [range_map]
exact Submodule.map₂_le_map₂ hab hcd
