instMulPosReflectLT

Mathlib.Data.EReal.Inv

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

English

Multiplication by a positive element reflects non-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 : MulPosReflectLT EReal :=
  MulPosMono.toMulPosReflectLT

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

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

Разделы

Аффилиация

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