preimage_floor_singleton

Mathlib.Algebra.Order.Floor.Ring

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

English

The preimage of a singleton under floor is exactly Ico(m, m+1).

Русский

Обратное изображение константы floor на одиночный элемент — это Ico(m, m+1).

LaTeX

$$$$ (\\mathrm{preimage} \\mathrm{floor} \\{ m \\}) = \\mathrm{Ico}(m, m+1) $$$$

Lean4

@[simp]
theorem preimage_floor_singleton (m : ℤ) : (floor : R → ℤ) ⁻¹' { m } = Ico (m : R) (m + 1) :=
  ext fun _ => floor_eq_iff

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

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

Разделы

Аффилиация

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