cast_mono — Mathlib

English

The integer embedding into any ordered ring is monotone: if m ≤ n then m cast ≤ n cast.

Русский

Целочисленное отображение в упорядоченное кольцо монотонно: если m ≤ n, то m.cast ≤ n.cast.

LaTeX

$$$m \le n \;\Rightarrow\; m^{\mathsf{cast}} \le n^{\mathsf{cast}}$$$

Lean4

theorem cast_mono : Monotone (Int.cast : ℤ → R) := by
  intro m n h
  rw [← sub_nonneg] at h
  lift n - m to ℕ using h with k hk
  rw [← sub_nonneg, ← cast_sub, ← hk, cast_natCast]
  exact k.cast_nonneg'

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