toSubsemigroup_strictMono — Mathlib

English

The map S ↦ toSubsemigroup(S) is strictly monotone with respect to inclusion: S < T implies toSubsemigroup(S) < toSubsemigroup(T).

Русский

Отображение S ↦ toSubsemigroup(S) строго монотонно по включению: S < T ⇒ toSubsemigroup(S) < toSubsemigroup(T).

LaTeX

$$$\forall R\,[\text{NonUnitalNonAssocRing } R],\forall S,T : \text{NonUnitalSubring } R,\ S < T \Rightarrow toSubsemigroup(S) < toSubsemigroup(T).$$$

Lean4

@[mono]
theorem toSubsemigroup_strictMono : StrictMono (toSubsemigroup : NonUnitalSubring R → Subsemigroup R) := fun _ _ => id

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