lt_tsub_iff_left_of_le

Mathlib.Algebra.Order.Sub.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#lt_tsub_iff_left_of_le

← MathLib Explorer

English

If c ≤ b, then a < b − c is equivalent to c + a < b.

Русский

Если c ≤ b, то a < b − c эквивалентно c + a < b.

LaTeX

$$$\forall a,b,c \in \alpha\,(c \le b) \Rightarrow (a < b - c \iff c + a < b)$$$

Lean4

/-- See `lt_tsub_iff_left` for a stronger statement in a linear order. -/
theorem lt_tsub_iff_left_of_le (h : c ≤ b) : a < b - c ↔ c + a < b :=
  Contravariant.AddLECancellable.lt_tsub_iff_left_of_le h

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

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

Разделы

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

Аффилиация

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