floor — Mathlib

English

In any ring α with a linear order and a FloorRing structure, the floor map is the standard floor: for every a, ⌊a⌋ is the greatest integer not exceeding a.

Русский

В любом кольце α с линейным порядком и структурой FloorRing функция floor есть стандартное округление вниз: для каждого a ⌊a⌋ — наибольшее целое число, не превосходящее a.

LaTeX

$$$\forall a \in \alpha,\; \lfloor a \rfloor = \max\{ z \in \mathbb{Z} \mid z \le a \}.$$$

Lean4

/-- `Int.floor a` is the greatest integer `z` such that `z ≤ a`. It is denoted with `⌊a⌋`. -/
def floor : α → ℤ :=
  FloorRing.floor

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