ceil_lt_add_one

Mathlib.Algebra.Order.Floor.Semiring

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

English

For ha ≥ 0, (⌈a⌉₊) < a + 1.

Русский

Для a ≥ 0 верно, что ⌈a⌉₊ < a + 1.

LaTeX

$$$$ \\lceil a \\rceil_+ < a + 1 $$$$

Lean4

@[bound]
theorem ceil_lt_add_one (ha : 0 ≤ a) : (⌈a⌉₊ : R) < a + 1 :=
  lt_ceil.1 <| (Nat.lt_succ_self _).trans_le (ceil_add_one ha).ge

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

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

Разделы

Аффилиация

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