one_le_div_iff — Mathlib

English

1 < a/b is equivalent to a/b < 1 under appropriate sign cases, expressed via standard sign-case decomposition.

Русский

1 < a/b эквивалентно a/b < 1 в подходящих случаях знака, выражено через разбиение по знаку.

LaTeX

$$Iff (1 < a/b) (0 < b ∧ b < a ∨ b < 0 ∧ a < b)$$

Lean4

theorem one_le_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_le_div_of_neg]
  · simp [zero_lt_one.not_ge]
  · simp [hb, hb.not_gt, one_le_div]

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