ceil_lt_add_one_of_gt_neg_one — Mathlib

English

Let R be a linearly ordered ring endowed with a floor operation. If a > −1, then the ceiling of a satisfies ⌈a⌉ < a + 1.

Русский

Пусть R — линейно упорядоченное кольцо с операцией округления вверх. Для любого a > −1 выполняется ⌈a⌉ < a + 1.

LaTeX

$$$$ (-1 < a) \Rightarrow \lceil a \rceil_+ < a + 1 $$$$

Lean4

/-- a variant of `Nat.ceil_lt_add_one` with its condition `0 ≤ a` generalized to `-1 < a` -/
@[bound]
theorem ceil_lt_add_one_of_gt_neg_one (ha : -1 < a) : ⌈a⌉₊ < a + 1 :=
  by
  by_cases h : 0 ≤ a
  · exact ceil_lt_add_one h
  · rw [ceil_eq_zero.mpr (le_of_not_ge h), cast_zero]
    exact neg_lt_iff_pos_add.mp ha

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