range_cast_int — Mathlib

English

The image of the natural-to-integer cast is exactly the set of nonnegative integers inside ℤ.

Русский

Образ нат-от-к-целое отображение равен множеству неотрицательных целых чисел внутри ℤ.

LaTeX

$$$ \operatorname{Set.range}(\mathrm{Nat.cast}) = \mathrm{Ici}(0) \subseteq \mathbb{Z} $$$

Lean4

@[simp]
theorem range_cast_int : range ((↑) : ℕ → ℤ) = Ici 0 :=
  Subset.antisymm (range_subset_iff.2 Int.natCast_nonneg) CanLift.prf

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