floor_mono

Mathlib.Algebra.Order.Floor.Ring

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

English

The floor function is monotone: a ≤ b implies ⌊a⌋ ≤ ⌊b⌋.

Русский

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

LaTeX

$$$$ a \\le b \\Rightarrow \\lfloor a \\rfloor \\le \\lfloor b \\rfloor $$$$

Lean4

@[mono]
theorem floor_mono : Monotone (floor : R → ℤ) :=
  gc_coe_floor.monotone_u

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

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

Разделы

Аффилиация

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