le_div — Mathlib

English

For all a,b,c, c ≠ 0 implies a ≤ b / c iff c · a ≤ b (left-cancellation form).

Русский

Для всех a,b,c, c ≠ 0, а ≤ b / c тогда и только тогда, когда c · a ≤ b (левая форма).

LaTeX

$$$\forall a,b,c \in \mathrm{Ordinal},\ c \neq 0 \rightarrow (a \le b / c \Leftrightarrow c \cdot a \le b)$$$

Lean4

theorem le_div {a b c : Ordinal} (c0 : c ≠ 0) : a ≤ b / c ↔ c * a ≤ b := by
  induction a using limitRecOn with
  | zero => simp only [mul_zero, Ordinal.zero_le]
  | succ _ _ => rw [succ_le_iff, lt_div c0]
  | limit _ h₁ h₂ =>
    revert h₁ h₂
    simp +contextual only [mul_le_iff_of_isSuccLimit, IsSuccLimit.le_iff_forall_le, forall_true_iff]

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