addLeftReflectLT

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.addLeftReflectLT

English

For ENNReal, addition on the left reflects strict order: a + b < a + c implies b < c when a is finite.

Русский

Для ENNReal сложение слева сохраняет строгое неравенство: a + b < a + c → b < c при конечном a.

LaTeX

$$AddLeftReflectLT ENNReal$$

Lean4

instance addLeftReflectLT : AddLeftReflectLT ℝ≥0∞ :=
  WithTop.addLeftReflectLT

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

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

Разделы

Аффилиация

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