toSubsemiring_strictMono — Mathlib

English

StrictMonotone property of the map toSubsemiring: Subring R → Subsemiring R is strictly monotone.

Русский

Строго монотонное отображение: Subring R → Subsemiring R сохраняет строгую монотонность.

LaTeX

$$$\text{toSubsemiring}: \text{Subring}(R) \to \text{Subsemiring}(R) \text{ is StrictMono}$$$

Lean4

@[mono]
theorem toSubsemiring_strictMono : StrictMono (toSubsemiring : Subring R → Subsemiring R) := fun _ _ => id

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