floor_lt_ceil_of_lt — Mathlib

English

Let a and b be elements of an ordered ring with floor and ceiling operations. If a < b, then ⌊a⌋ < ⌈b⌉.

Русский

Пусть a и b — элементы упорядоченного кольца с операциями floor и ceil. Если a < b, то ⌊a⌋ < ⌈b⌉.

LaTeX

$$$a < b \\implies \\lfloor a \\rfloor < \\lceil b \\rceil$$$

Lean4

@[bound]
theorem floor_lt_ceil_of_lt {a b : R} (h : a < b) : ⌊a⌋ < ⌈b⌉ :=
  cast_lt.1 <| (floor_le a).trans_lt <| h.trans_le <| le_ceil b

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