ceil_eq_iff — Mathlib

English

If n ≠ 0, then ⌈a⌉₊ = n holds exactly when (n − 1) < a ≤ n.

Русский

Если n ≠ 0, то ⌈a⌉₊ = n эквивалентно (n − 1) < a ≤ n.

LaTeX

$$$ n \neq 0 \Rightarrow (\lceil a \rceil_{+} = n) \iff ((n-1) : \mathbb{R}) < a \land a \le n $$$

Lean4

theorem ceil_eq_iff (hn : n ≠ 0) : ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ n := by
  rw [← ceil_le, ← not_le, ← ceil_le, not_le, tsub_lt_iff_right (Nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)),
    Nat.lt_add_one_iff, le_antisymm_iff, and_comm]

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