natCast — Mathlib

English

There is a natural-number cast on the nonnegative subtype, mapping n to the corresponding nonnegative element.

Русский

Существуют отображение натуральных чисел в подтип неотрицательных элементов, переводя n в соответствующий элемент.

LaTeX

$$$ \text{NatCast} \; { x : \alpha // 0 \le x } $$$

Lean4

instance natCast : NatCast { x : α // 0 ≤ x } :=
  ⟨fun n => ⟨n, Nat.cast_nonneg' n⟩⟩

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