lt_tsub_iff_left — Mathlib

English

For a, b, c in α with LinearOrder and OrderedSub, a < b − c is equivalent to c + a < b.

Русский

Для a, b, c ∈ α при линейном порядке и упорядоченном вычитании: a < b − c эквивалентно c + a < b.

LaTeX

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

Lean4

/-- See `lt_tsub_iff_left_of_le` for a weaker statement in a partial order. -/
theorem lt_tsub_iff_left : a < b - c ↔ c + a < b :=
  lt_iff_lt_of_le_iff_le tsub_le_iff_left

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