floor_le_ceil

Mathlib.Algebra.Order.Floor.Semiring

URI: https://scilib.ai/kg/mathlib#Nat.floor_le_ceil

← MathLib Explorer

English

For every a, floor a ≤ ceil a.

Русский

Для любого a выполняется ⌊a⌋ ≤ ⌈a⌉.

LaTeX

$$$\lfloor a \rfloor \le \lceil a \rceil$$$

Lean4

@[bound]
theorem floor_le_ceil (a : R) : ⌊a⌋₊ ≤ ⌈a⌉₊ :=
  by
  obtain ha | ha := le_total a 0
  · rw [floor_of_nonpos ha]
    exact Nat.zero_le _
  · exact cast_le.1 ((floor_le ha).trans <| le_ceil _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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