instFloorRing — Mathlib

English

The real numbers carry a floor operation: for every x ∈ ℝ there exists an integer ub with ub ≤ x and every integer z ≤ x satisfies z ≤ ub; i.e., ⌊x⌋ is the greatest integer not exceeding x.

Русский

У вещественных чисел есть операция целого снизу: для каждого x ∈ ℝ существует целое ub такое, что ub ≤ x и для любого z ∈ ℤ с z ≤ x следует z ≤ ub; то есть ⌊x⌋ — наибольшее целое не превосходящее x.

LaTeX

$$$\exists ub \in \mathbb{Z},\; ub \le x \wedge \forall z \in \mathbb{Z},\; z \le x \rightarrow z \le ub$$$

Lean4

noncomputable instance : FloorRing ℝ :=
  Archimedean.floorRing _

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