instIntCast — Mathlib

English

If β has an IntCast, then there is an IntCast instance on α →ᵇ β sending m to the constant function with value m.

Русский

Если β имеет IntCast, то на α →ᵇ β есть инстанс IntCast: m ↦ константная функция со значением m.

LaTeX

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

Lean4

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

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