natCast_div_le — Mathlib

English

For m,n ∈ ℕ, the natural division (m/n) as a natural number is ≤ the division of their EReal embeddings: (m / n)_Nat ≤ (m:EReal) / (n:EReal).

Русский

Для m,n ∈ ℕ целочисленное деление m/n не более чем деление чисел m и n после отображения в EReal.

LaTeX

$$$ \bigl(m / n\bigr) \\leq (m:EReal) / (n:EReal) $$$

Lean4

theorem natCast_div_le (m n : ℕ) : (m / n : ℕ) ≤ (m : EReal) / (n : EReal) :=
  by
  rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_div, EReal.coe_le_coe_iff]
  exact Nat.cast_div_le

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