le_sub_iff_add_le_left

Mathlib.Data.ENNReal.Operations

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

← MathLib Explorer

English

For c ≠ ∞ and c ≤ b, a ≤ b − c iff c + a ≤ b.

Русский

Для c ≠ ∞ и c ≤ b: a ≤ b − c эквивалентно c + a ≤ b.

LaTeX

$$$$ c \neq \infty \land c \le b \Rightarrow (a \le b - c \iff c + a \le b). $$$$

Lean4

theorem le_sub_iff_add_le_left (hc : c ≠ ∞) (hcb : c ≤ b) : a ≤ b - c ↔ c + a ≤ b :=
  ⟨fun h ↦ add_le_of_le_tsub_left_of_le hcb h, le_sub_of_add_le_left hc⟩

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

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

Разделы

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

Аффилиация

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