div_le_one_iff — Mathlib

English

For all a,b, a/b ≤ 1 is equivalent to 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_le_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_le_one_of_neg]
  · simp [zero_le_one]
  · simp [hb, hb.not_gt, div_le_one, hb.ne.symm]

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