floorDiv_le_ceilDiv — Mathlib

English

For all b, floorDiv by a is ≤ ceilDiv by a: b ⌊/⌋ a ≤ b ⌈/⌉ a.

Русский

Для всех b ≤, floorDiv по a не превосходит ceilDiv по a: b ⌊/⌋ a ≤ b ⌈/⌉ a.

LaTeX

$$$ b \\\\ll floor / a \\\\rr \\\\le b \\\\lceil/ a \\\\rceil.$$$

Lean4

theorem floorDiv_le_ceilDiv : b ⌊/⌋ a ≤ b ⌈/⌉ a :=
  by
  obtain ha | ha := le_or_gt a 0
  · simp [ha]
  · exact le_of_smul_le_smul_left ((smul_floorDiv_le ha).trans <| le_smul_ceilDiv ha) ha

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