instPosMulReflectLT

Mathlib.Data.EReal.Inv

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

English

Multiplication by a positive element reflects strict order: if a < b, then c a < c b for c > 0.

Русский

Умножение на положительное число отображает строгий порядок: если a < b, то c a < c b для c > 0.

LaTeX

$$∀ a,b,c ∈ EReal, c > 0 ∧ a < b ⇒ c a < c b$$

Lean4

instance : PosMulReflectLT EReal :=
  PosMulMono.toPosMulReflectLT

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

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

Разделы

Аффилиация

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