ceil_eq_on_Ioc

Mathlib.Algebra.Order.Floor.Ring

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

English

If a lies in the interval (z−1, z], then ceil(a) = z.

Русский

Если a лежит в промежутке (z−1, z], то ⌈a⌉ = z.

LaTeX

$$$a \\in (z-1, z] \\\\Rightarrow \\\\lceil a\\\\rceil = z$$$

Lean4

theorem ceil_eq_on_Ioc (z : ℤ) : ∀ a ∈ Set.Ioc (z - 1 : R) z, ⌈a⌉ = z := fun _ ⟨h₀, h₁⟩ => ceil_eq_iff.mpr ⟨h₀, h₁⟩

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

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

Разделы

Аффилиация

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