toMulPosMono

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs

URI: https://scilib.ai/kg/mathlib#MulPosReflectLT.toMulPosMono

English

From MulPosReflectLT α deduce MulPosMono α.

Русский

Из MulPosReflectLT α следует MulPosMono α.

LaTeX

$$MulPosReflectLT(\alpha) \Rightarrow MulPosMono(\alpha)$$

Lean4

theorem toMulPosMono [MulPosReflectLT α] : MulPosMono α where
  elim := (covariant_le_iff_contravariant_lt _ _ _).2 ContravariantClass.elim

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

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

Разделы

Аффилиация

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