lt_div

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.lt_div

English

For c ≠ 0, a < b / c iff c · succ a ≤ b.

Русский

Для c ≠ 0 верно: a < b / c тогда и только тогда, когда c · succ a ≤ b.

LaTeX

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

Lean4

theorem lt_div {a b c : Ordinal} (h : c ≠ 0) : a < b / c ↔ c * succ a ≤ b := by rw [← not_le, div_le h, not_lt]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru