English
For every real x there exists an integer ub such that ub ≤ x and every integer z with 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
theorem exists_floor (x : ℝ) : ∃ ub : ℤ, (ub : ℝ) ≤ x ∧ ∀ z : ℤ, (z : ℝ) ≤ x → z ≤ ub :=
Int.exists_greatest_of_bdd
(let ⟨n, hn⟩ := exists_int_gt x
⟨n, fun _ h' => Int.cast_le.1 <| le_trans h' <| le_of_lt hn⟩)
(let ⟨n, hn⟩ := exists_int_lt x
⟨n, le_of_lt hn⟩)
