div_lt — Mathlib

English

Let a, b, c be ordinals with b ≠ 0. Then a / b < c if and only if a < b · c.

Русский

Пусть a, b и c — ординалы и b ≠ 0. Тогда a / b < c тогда и только тогда, когда a < b · c.

LaTeX

$$$\\\\forall a,b,c \\\\\\in \\operatorname{Ord},\\\\ b \\\\\\neq 0 \\\\\\Rightarrow (\\\\frac{a}{b} < c) \\\\\\Leftrightarrow (a < b \\\\\\cdot c)$$$

Lean4

theorem div_lt {a b c : Ordinal} (b0 : b ≠ 0) : a / b < c ↔ a < b * c :=
  lt_iff_lt_of_le_iff_le <| le_div b0

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