mk_natCast — Mathlib

English

Embedding a natural number into the nonnegative subtype via its obvious witness; this equals the corresponding element.

Русский

Вложение натурального числа в подтип через очевидное доказательство неотрицательности; равняется соответствующему элементу.

LaTeX

$$$ (\langle n, n \ge 0 \rangle) = n $$$

Lean4

@[simp]
theorem mk_natCast (n : ℕ) : (⟨n, n.cast_nonneg'⟩ : { x : α // 0 ≤ x }) = n :=
  rfl

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