toSubmonoid_mono — Mathlib

English

Let R be a ring. The map s ↦ s.toSubmonoid is monotone: if S ⊆ T then S.toSubmonoid ⊆ T.toSubmonoid.

Русский

Пусть R — кольцо. Отображение S ↦ S.toSubmonoid монотонно: если S ⊆ T, то S.toSubmonoid ⊆ T.toSubmonoid.

LaTeX

$$$\\forall S,T \\subseteq R:\\ S \\subseteq T \\Rightarrow S_{\\mathrm{Mon}} \\subseteq T_{\\mathrm{Mon}}.$$$

Lean4

@[mono]
theorem toSubmonoid_mono : Monotone (fun s : Subring R => s.toSubmonoid) :=
  toSubmonoid_strictMono.monotone

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