sub_le_sub_iff_left

Mathlib.Data.ENNReal.Operations

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

← MathLib Explorer

English

If c ≤ a and a ≠ ∞, then a − b ≤ a − c iff c ≤ b.

Русский

Если c ≤ a и a ≠ ∞, то a − b ≤ a − c тогда и только если c ≤ b.

LaTeX

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

Lean4

theorem sub_le_sub_iff_left (h : c ≤ a) (h' : a ≠ ∞) : (a - b ≤ a - c) ↔ c ≤ b :=
  (cancel_of_ne h').tsub_le_tsub_iff_left (cancel_of_ne (ne_top_of_le_ne_top h' h)) h

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

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

Разделы

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

Аффилиация

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