lt_succ_floor

Mathlib.Algebra.Order.Floor.Semiring

URI: https://scilib.ai/kg/mathlib#Nat.lt_succ_floor

English

For every element a in a linearly ordered ring with a floor operation, one has a < floor(a) + 1.

Русский

Для любого элемента a в линейно упорядоченном кольце с операцией floor выполняется неравенство a < floor(a) + 1.

LaTeX

$$$a < \lfloor a \rfloor_+ + 1$$$

Lean4

theorem lt_succ_floor (a : R) : a < ⌊a⌋₊.succ :=
  lt_of_floor_lt <| Nat.lt_succ_self _

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

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

Разделы

Аффилиация

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