ceil_eq_iff — Mathlib

English

Let a be an element of the real-ordered ring R and z an integer. Then ceil(a) = z if and only if z − 1 < a ≤ z.

Русский

Пусть a принадлежит R и z ∈ ℤ. Тогда ⌈a⌉ = z тогда и только тогда, когда z−1 < a ≤ z.

LaTeX

$$$\\\\lceil a\\\\rceil = z \\\\iff z-1 < a \\\\le z$$$

Lean4

theorem ceil_eq_iff : ⌈a⌉ = z ↔ ↑z - 1 < a ∧ a ≤ z := by
  rw [← ceil_le, ← Int.cast_one, ← Int.cast_sub, ← lt_ceil, Int.sub_one_lt_iff, le_antisymm_iff, and_comm]

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