mulRightMono_of_mulRightStrictMono

Mathlib.Algebra.Order.Monoid.Unbundled.Defs

URI: https://scilib.ai/kg/mathlib#mulRightMono_of_mulRightStrictMono

← MathLib Explorer

English

If right translations are strictly monotone, then right translations are monotone.

Русский

Если правые переносы строго монотонны, то они монотонны.

LaTeX

$$$\text{RightMono}(M) \Rightarrow \text{RightMono}(M)$$$

Lean4

@[to_additive]
theorem mulRightMono_of_mulRightStrictMono (M) [Mul M] [PartialOrder M] [MulRightStrictMono M] : MulRightMono M :=
  covariantClass_le_of_lt _ _ _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru