ceil_add_one

Mathlib.Algebra.Order.Floor.Ring

URI: https://scilib.ai/kg/mathlib#Int.ceil_add_one

English

For any a ∈ R, ceil(a + 1) = ceil(a) + 1.

Русский

Для любого a ∈ R, ceil(a + 1) = ceil(a) + 1.

LaTeX

$$$\\\\lceil a + 1 \\\\rceil = \\\\lceil a \\\\rceil + 1$$$

Lean4

@[simp]
theorem ceil_add_one (a : R) : ⌈a + 1⌉ = ⌈a⌉ + 1 := by rw [← ceil_add_intCast a (1 : ℤ), cast_one]

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

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

Разделы

Аффилиация

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