English
In a ring R with order, that is Archimedean, every x ∈ R has an integer floor fl ∈ ℤ such that for all z ∈ ℤ, z ≤ fl iff (z : R) ≤ x.
Русский
В упорядоченном кольце R с архимедовым свойством каждому x ∈ R соответствует целое floor x ∈ ℤ, такое что для всех z ∈ ℤ выполняется z ≤ ⌊x⌋ тогда и только тогда z ≤ x.
LaTeX
$$$\\exists fl ∈ \\mathbb{Z}, \\forall z \\in \\mathbb{Z}, (z \\le fl) \\iff ((z : R) \\le x)$$$
Lean4
theorem exists_floor (x : R) : ∃ fl : ℤ, ∀ z : ℤ, z ≤ fl ↔ (z : R) ≤ x := by
classical
have : ∃ ub : ℤ, (ub : R) ≤ x ∧ ∀ z : ℤ, (z : R) ≤ x → z ≤ ub :=
Int.exists_greatest_of_bdd
(let ⟨n, hn⟩ := exists_int_gt x
⟨n, fun z h' => Int.cast_le.1 <| le_trans h' <| le_of_lt hn⟩)
(let ⟨n, hn⟩ := exists_int_lt x
⟨n, le_of_lt hn⟩)
refine this.imp fun fl h z => ?_
obtain ⟨h₁, h₂⟩ := h
exact ⟨fun h => le_trans (Int.cast_le.2 h) h₁, h₂ z⟩
