tsub_lt_tsub_iff_left_of_le_of_le

English

For b ≤ a and c ≤ a, a − b < a − c ↔ c < b, provided a structure reflects LT from left.

Русский

Для b ≤ a и c ≤ a, при условии, что левая редукция сохраняет порядок, a − b < a − c ↔ c < b.

LaTeX

$$$\forall a,b,c \in \alpha\,[b \le a] [c \le a] : a - b < a - c \iff c < b$$$

Lean4

/-- See `tsub_lt_tsub_iff_left_of_le` for a stronger statement in a linear order. -/
theorem tsub_lt_tsub_iff_left_of_le_of_le [AddLeftReflectLT α] (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < a - c ↔ c < b :=
  Contravariant.AddLECancellable.tsub_lt_tsub_iff_left_of_le_of_le Contravariant.AddLECancellable h₁ h₂

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