toAddSubgroup_mono — Mathlib

English

The map S ↦ toAddSubgroup(S) is monotone with respect to inclusion of nonunital subrings: if S ≤ T then toAddSubgroup(S) ≤ toAddSubgroup(T).

Русский

Отображение S ↦ toAddSubgroup(S) монотонно по включению: если S ⊆ T, то toAddSubgroup(S) ⊆ toAddSubgroup(T).

LaTeX

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

Lean4

@[mono]
theorem toAddSubgroup_mono : Monotone (toAddSubgroup : NonUnitalSubring R → AddSubgroup R) :=
  toAddSubgroup_strictMono.monotone

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