instNatCast_1 — Mathlib

English

There is a natural-number casting for bounded continuous functions, given by the constant embedding.

Русский

Существует отображение приведения к натуральному числу для ограниченных непрерывных функций через константное внедрение.

LaTeX

$$$\\text{NatCast}$ (BoundedContinuousFunction α R) defined by n \\mapsto \\mathrm{const}_{\\alpha} n$$$

Lean4

instance : NatCast (α →ᵇ R) :=
  ⟨fun n => BoundedContinuousFunction.const _ n⟩

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