coe_natCast — Mathlib

English

The coercion of a natural number into the nonnegative subtype followed by the ambient coercion equals the natural number itself.

Русский

Приведение натурального числа к подтипу неотрицательных элементов, затем к базовому типу, даёт само число.

LaTeX

$$$ ↑(n) : \alpha = n $$$

Lean4

@[simp, norm_cast]
protected theorem coe_natCast (n : ℕ) : ((↑n : { x : α // 0 ≤ x }) : α) = n :=
  rfl

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