toSubMulAction_strictMono — Mathlib

English

The map p ↦ toSubMulAction is strictly monotone with respect to inclusion.

Русский

Отображение p ↦ toSubMulAction строго монотонно по включению.

LaTeX

$$$\text{toSubMulAction}: \text{Submodule} \to \text{SubMulAction}$ является строгим монотонным отображением.$$

Lean4

@[mono]
theorem toSubMulAction_strictMono : StrictMono (toSubMulAction : Submodule R M → SubMulAction R M) := fun _ _ => id

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