English
Let z ∈ ℤ and r ∈ ℚ. Then z ≤ ⌊r⌋ if and only if (z as ℚ) ≤ r.
Русский
Пусть z ∈ ℤ и r ∈ ℚ. Тогда z ≤ ⌊r⌋ тогда и только тогда, когда z ≤ r (в полезночной шкале).
LaTeX
$$$z \in \mathbb{Z}, r \in \mathbb{Q} \Rightarrow z \le \lfloor r \rfloor \iff (z \le r)$$$
Lean4
@[deprecated Rat.le_floor_iff (since := "2025-09-02")]
protected theorem le_floor {z : ℤ} : ∀ {r : ℚ}, z ≤ Rat.floor r ↔ (z : ℚ) ≤ r
| ⟨n, d, h, c⟩ => by
simp only [Rat.floor_def]
rw [mk'_eq_divInt]
have h' := Int.ofNat_lt.2 (Nat.pos_of_ne_zero h)
conv =>
rhs
rw [intCast_eq_divInt, Rat.divInt_le_divInt zero_lt_one h', mul_one]
exact Int.le_ediv_iff_mul_le h'
