instNatCast

Mathlib.Topology.LocallyConstant.Algebra

URI: https://scilib.ai/kg/mathlib#LocallyConstant.instNatCast

English

LocallyConstant X Y has a natural-number embedding: n ↦ const_X(n).

Русский

LocallyConstant X Y имеет вложение натуральных чисел: n ↦ константная функция n по всем точкам.

LaTeX

$$$\text{natCast}(n) = \text{const}_X(n).$$$

Lean4

instance [NatCast Y] : NatCast (LocallyConstant X Y) where natCast n := const X n

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

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

Разделы

Аффилиация

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