lt_tsub_comm

Mathlib.Algebra.Order.Sub.Defs

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

English

In a linear ordered setting, a < b − c is equivalent to c < b − a.

Русский

В линейно упорядоченном контексте a < b − c эквивалентно c < b − a.

LaTeX

$$$a < b - c \\iff c < b - a$$$

Lean4

theorem lt_tsub_comm : a < b - c ↔ c < b - a :=
  lt_tsub_iff_left.trans lt_tsub_iff_right.symm

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

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

Разделы

Аффилиация

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