mono_cast — Mathlib

English

The natural-number casting map Nat.cast: ℕ → α is monotone with respect to the order on α, i.e. if m ≤ n then m ≤ n in α after casting.

Русский

Отображение Nat.cast: ℕ → α монотонно по отношению к порядку на α: если m ≤ n, то m^↦ ≤ n^↦ в α.

LaTeX

$$$\forall m,n \in \mathbb{N},\ m \le n \Rightarrow (m : \alpha) \le (n : \alpha)$.$$

Lean4

@[mono]
theorem mono_cast : Monotone (Nat.cast : ℕ → α) :=
  monotone_nat_of_le_succ fun n ↦ by rw [Nat.cast_succ]; exact le_add_of_nonneg_right zero_le_one

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