div_le — Mathlib

English

If IsSuccLimit b, then a · b ≤ c iff ∀ b' < b, a · b' ≤ c.

Русский

Если IsSuccLimit b, то a · b ≤ c тогда и только тогда, когда ∀ b' < b, a · b' ≤ c.

LaTeX

$$$\forall a,b,c \in \mathrm{Ordinal},\ IsSuccLimit(b) \rightarrow (a \cdot b \le c \iff \forall b' < b,\ a \cdot b' \le c)$$$

Lean4

theorem div_le {a b c : Ordinal} (b0 : b ≠ 0) : a / b ≤ c ↔ a < b * succ c :=
  ⟨fun h => (lt_mul_succ_div a b0).trans_le (mul_le_mul_left' (succ_le_succ_iff.2 h) _), fun h => by rw [div_def a b0];
    exact csInf_le' h⟩

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