coe_natCast — Mathlib

English

Natural numbers embed into SimpleFunc via constant functions: the nth natural is the constant function with value n.

Русский

Естественные числа инкорпорируются в SimpleFunc через константные функции: n-й натуральный — константа n.

LaTeX

$$$\\text{coe\_natCast } [NatCast \\beta] (n: \\mathbb{N}) : \\; \\⇑(↑n : \\alpha \\to_{S} \\beta) = \\text{fun } _ \\mapsto n.$$$

Lean4

@[simp, norm_cast]
theorem coe_natCast [NatCast β] (n : ℕ) : ⇑(↑n : α →ₛ β) = fun _ ↦ ↑n :=
  rfl

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