natCast_le_cast — Mathlib

English

For m ∈ ℕ and n ∈ ℚ≥0, the inequality between their casts in K corresponds to the inequality in ℚ≥0, i.e., m.cast ≤ n.cast is equivalent to m.cast ≤ n in ℚ≥0 order.

Русский

Для m ∈ ℕ и n ∈ ℚ≥0: неравенство m.cast ≤ n.cast в K эквивалентно неравенству m.cast ≤ n в порядке ℚ≥0.

LaTeX

$$$(m \text{ cast}) \le (n \text{ cast}) \iff m \le n$ в соответствующем порядке ℚ≥0$$

Lean4

@[simp, norm_cast]
theorem natCast_le_cast {m : ℕ} {n : ℚ≥0} : (m : K) ≤ n ↔ (m : ℚ≥0) ≤ n := by rw [← cast_le (K := K), cast_natCast]

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