coe_natCast — Mathlib

English

The natural numbers embed into WithTop α by the natural cast, i.e., (n : α) → WithTop α remains the same under the embedding.

Русский

Естественные числа вкладываются в WithTop α через естественное отображение, то есть (n : α) → WithTop α сохраняется при вложении.

LaTeX

$$$\\\\forall n : \\\\mathbb{N}, \\\\text{coe_natCast}: ((n : α) : WithTop α) = n$$$

Lean4

@[simp, norm_cast]
theorem coe_natCast (n : ℕ) : ((n : α) : WithTop α) = n :=
  rfl

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