lt_mul_div_add

Mathlib.SetTheory.Ordinal.Arithmetic

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

English

For all a and nonzero b, a < b · (a / b) + b.

Русский

Для любых a и не нуля b, выполняется a < b · (a / b) + b.

LaTeX

$$$\forall a \in \mathrm{Ordinal},\ \forall b \in \mathrm{Ordinal},\ b \neq 0 \rightarrow a < b \cdot (a / b) + b$$$

Lean4

theorem lt_mul_div_add (a) {b : Ordinal} (h : b ≠ 0) : a < b * (a / b) + b := by
  simpa only [mul_succ] using lt_mul_succ_div a h

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

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

Разделы

Аффилиация

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