preimage_ceil_singleton

Mathlib.Algebra.Order.Floor.Ring

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

English

The set of all x with ceil(x) = m is exactly the interval (m−1, m].

Русский

Множество всех x с ceil(x) = m равно интервалу (m−1, m].

LaTeX

$$$\\\\{ x \\\\in \\mathbb{R} : \\\\lceil x\\\\rceil = m \\\\} = (m-1, m]$$$

Lean4

@[simp]
theorem preimage_ceil_singleton (m : ℤ) : (ceil : R → ℤ) ⁻¹' { m } = Ioc ((m : R) - 1) m :=
  ext fun _ => ceil_eq_iff

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

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

Разделы

Аффилиация

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