ceil — Mathlib

English

The ceiling function on a general ordered ring yields the least natural number not less than a, i.e. ⌈a⌉₊.

Русский

Округление вверх в общем упорядоченном кольце даёт наименьшее натуральное число, не меньшeе a, то есть ⌈a⌉₊.

LaTeX

$$$\text{ceil}:\alpha \to \mathbb{N} \text{ is the FloorSemiring.ceil function.}$$$

Lean4

/-- `⌈a⌉₊` is the least natural `n` such that `a ≤ n` -/
def ceil : α → ℕ :=
  FloorSemiring.ceil

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