add_lt_add

Mathlib.Data.ENNReal.Operations

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

← MathLib Explorer

English

If a < c and b < d then a + b < c + d.

Русский

Если a < c и b < d, то a + b < c + d.

LaTeX

$$$a < c \land b < d \Rightarrow a + b < c + d$$$

Lean4

@[gcongr]
protected theorem add_lt_add (ac : a < c) (bd : b < d) : a + b < c + d :=
  by
  lift a to ℝ≥0 using ac.ne_top
  lift b to ℝ≥0 using bd.ne_top
  cases c; · simp
  cases d; · simp
  simp only [← coe_add, coe_lt_coe] at *
  exact add_lt_add ac bd

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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