tsub_lt_tsub_iff_left_of_le_of_le

English

With AddLECancellable b and AddLECancellable (a − b), if b ≤ a and c ≤ a, then a − b < a − c iff c < b.

Русский

При AddLECancellable(b) и AddLECancellable(a − b), если b ≤ a и c ≤ a, то a − b < a − c эквивалентно c < b.

LaTeX

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

Lean4

protected theorem tsub_lt_tsub_iff_left_of_le_of_le [AddLeftReflectLT α] (hb : AddLECancellable b)
    (hab : AddLECancellable (a - b)) (h₁ : b ≤ a) (h₂ : c ≤ a) : a - b < a - c ↔ c < b :=
  ⟨hb.lt_of_tsub_lt_tsub_left_of_le h₂, hab.tsub_lt_tsub_left_of_le h₁⟩

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