instIntCast_1

Mathlib.Topology.ContinuousMap.Bounded.Normed

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.instIntCast_1

English

There is an IntCast structure on α →ᵇ R given by the constant embedding.

Русский

Существует IntCast на α →ᵇ R задаваемый через константное внедрение.

LaTeX

$$$\\text{IntCast}$ (α →ᵇ R)$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru