floor_mono

Mathlib.Algebra.Order.Floor.Semiring

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

← MathLib Explorer

English

The floor function is monotone: if a ≤ b then floor(a) ≤ floor(b).

Русский

Функция floor монотонна: если a ≤ b, то ⌊a⌋₊ ≤ ⌊b⌋₊.

LaTeX

$$($a \le b) \Rightarrow (\lfloor a \rfloor_+ \le \lfloor b \rfloor_+$)$$

Lean4

theorem floor_mono : Monotone (floor : R → ℕ) := fun a b h =>
  by
  obtain ha | ha := le_total a 0
  · rw [floor_of_nonpos ha]
    exact Nat.zero_le _
  · exact le_floor ((floor_le ha).trans h)

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

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

Разделы

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

Аффилиация

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