instNatCast — Mathlib

English

If β has a natural number cast, then there is a NatCast instance on α →ᵇ β sending n to the constant function with value n.

Русский

Если β имеет отображение натурального числа в β, то на пространстве α →ᵇ β есть инстанс NatCast: n ↦ константная функция, равная n.

LaTeX

$$$[\text{NatCast }(\alpha \to^{\mathrm{b}} \beta)] : \mathbb{N} \to (\alpha \to^{\mathrm{b}} \beta)$$$

Lean4

instance [NatCast β] : NatCast (α →ᵇ β) :=
  ⟨fun n ↦ BoundedContinuousFunction.const _ n⟩

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