ceil_eq_on_Ioc'

Mathlib.Algebra.Order.Floor.Ring

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

English

For z ∈ ℤ and a ∈ (z−1, z], the real embedding of ceil(a) equals z.

Русский

Для z ∈ ℤ и a ∈ (z−1, z], вещественное отображение ceil(a) равно z.

LaTeX

$$$a \\in (z-1, z] \\\\Rightarrow \\\\lceil a \\\\rceil^{\\uparrow} = z^{\\uparrow}$$$

Lean4

theorem ceil_eq_on_Ioc' (z : ℤ) : ∀ a ∈ Set.Ioc (z - 1 : R) z, (⌈a⌉ : R) = z := fun a ha =>
  mod_cast ceil_eq_on_Ioc z a ha

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

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

Разделы

Аффилиация

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