one_lt_div_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem one_lt_div_iff : 1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b :=
  by
  rcases lt_trichotomy b 0 with (hb | rfl | hb)
  · simp [hb, hb.not_gt, one_lt_div_of_neg]
  · simp [zero_le_one]
  · simp [hb, hb.not_gt, one_lt_div]

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