cast_nonneg — Mathlib

English

For any integer n, n.cast ≥ 0 in R iff n ≥ 0 in Z.

Русский

Для любого целого числа n, n.cast ≥ 0 в R тогда и только тогда, когда n ≥ 0 в Z.

LaTeX

$$$n^{\mathsf{cast}} \ge 0 \iff n \ge 0$$$

Lean4

@[simp]
theorem cast_nonneg : ∀ {n : ℤ}, (0 : R) ≤ n ↔ 0 ≤ n
  | (n : ℕ) => by simp
  | -[n+1] => by
    have : -(n : R) < 1 := lt_of_le_of_lt (by simp) zero_lt_one
    simpa [(negSucc_lt_zero n).not_ge, ← sub_eq_add_neg, le_neg] using this.not_ge

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