lt_add_right

Mathlib.Data.ENNReal.Operations

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

English

If a ≠ ∞ and b ≠ 0, then a < a + b.

Русский

Если a ≠ ∞ и b ≠ 0, то a < a + b.

LaTeX

$$lt_add_right (ha : a ≠ ∞) (hb : b ≠ 0) : a < a + b$$

Lean4

theorem lt_add_right (ha : a ≠ ∞) (hb : b ≠ 0) : a < a + b := by
  rwa [← pos_iff_ne_zero, ← ENNReal.add_lt_add_iff_left ha, add_zero] at hb

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

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

Разделы

Аффилиация

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