div_le_of_le_mul — Mathlib

English

If a ≤ b · c, then a / b ≤ c (and if b = 0, then a / b = 0, which makes the inequality hold).

Русский

Если a ≤ b · c, то a / b ≤ c (и если b = 0, то a / b = 0, что обеспечивает неравенство).

LaTeX

$$$a, b, c \\\\\\in \\operatorname{Ord} \\\\Rightarrow \\\\ a \\\\\\le b \\\\\\cdot c \\\\Rightarrow \\\\ frac{a}{b} \\\\le c.$$$

Lean4

theorem div_le_of_le_mul {a b c : Ordinal} (h : a ≤ b * c) : a / b ≤ c :=
  if b0 : b = 0 then by simp only [b0, div_zero, Ordinal.zero_le]
  else (div_le b0).2 <| h.trans_lt <| mul_lt_mul_of_pos_left (lt_succ c) (Ordinal.pos_iff_ne_zero.2 b0)

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