div_lt_one_iff — Mathlib

English

For all a,b, a/b < 1 is equivalent to either 0 < b and a < b, or b = 0, or b < 0 and b < a.

Русский

Для любых a,b: a/b < 1 эквивалентно либо 0 < b и a < b, либо b = 0, либо b < 0 и b < a.

LaTeX

$$a/b < 1 ↔ (0 < b ∧ a < b) ∨ (b = 0) ∨ (b < 0 ∧ b < a)$$

Lean4

theorem div_lt_one_iff : a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a :=
  by
  rcases lt_trichotomy b 0 with (hb | rfl | hb)
  · simp [hb, hb.not_gt, hb.ne, div_lt_one_of_neg]
  · simp [zero_lt_one]
  · simp [hb, hb.not_gt, div_lt_one, hb.ne.symm]

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