Submodule.map₂_le_map₂

theorem Submodule.map₂_le_map₂ : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P] {f : M →ₗ[R] N →ₗ[R] P} {p₁ p₂ : Submodule R M} {q₁ q₂ : Submodule R N}, p₁ ≤ p₂ → q₁ ≤ q₂ → Submodule.map₂ f p₁ q₁ ≤ Submodule.map₂ f p₂ q₂

This theorem states that for all types R, M, N, P, where R is a commutative semiring, M, N, P are additive commutative monoids, and M, N, P are modules over R, and for all linear maps `f` from M to N to P, and for submodules p₁, p₂ of M and q₁, q₂ of N, if p₁ is a subset of p₂ and q₁ is a subset of q₂, then the submodule obtained by mapping p₁ and q₁ through `f` is a subset of the submodule obtained by mapping p₂ and q₂ through `f`. Essentially, it says that the mapping of submodules via a linear map respects the subset relation.

More concisely: Given commutative semirings R, and additive commutative monoids M, N, P that are R-modules, for all submodules p₁ ⊆ p₂ of M and q₁ ⊆ q₂ of N, the image of p₁ under a linear map from M to N is contained in the image of p₂ under the same linear map, and similarly for N and P. In other words, the mapping of submodules via a linear map respects the subset relation.