tsub_lt_self_iff — Mathlib

English

For an AddLECancellable a, a − b < a if and only if 0 < a and 0 < b.

Русский

Для AddLECancellable(a) верно: a − b < a тогда и только тогда, когда 0 < a и 0 < b.

LaTeX

$$$\forall a,b\ , AddLECancellable(a) \Rightarrow (a - b < a \iff (0 < a \land 0 < b))$$$

Lean4

protected theorem tsub_lt_self_iff (ha : AddLECancellable a) : a - b < a ↔ 0 < a ∧ 0 < b :=
  by
  refine ⟨fun h => ⟨(zero_le _).trans_lt h, (zero_le b).lt_of_ne ?_⟩, fun h => ha.tsub_lt_self h.1 h.2⟩
  rintro rfl
  rw [tsub_zero] at h
  exact h.false

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