instMulPosMono

Mathlib.Data.EReal.Inv

URI: https://scilib.ai/kg/mathlib#EReal.instMulPosMono

English

The multiplication by a positive element is order-preserving on EReal.

Русский

Умножение на положительное число сохраняет порядок на EReal.

LaTeX

$$∀ a,b,c ∈ EReal, a ≤ b ⇒ c a ≤ c b whenever c > 0$$

Lean4

instance : MulPosMono EReal :=
  posMulMono_iff_mulPosMono.1 inferInstance

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

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

Разделы

Аффилиация

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