eval

Mathlib.Topology.Category.Profinite.Nobeling.Basic

URI: https://scilib.ai/kg/mathlib#Profinite.NobelingProof.GoodProducts.eval

English

Evaluation on good products yields a LocallyConstant function into ℤ.

Русский

Оценивание для хороших продуктов даёт локально константную функцию в ℤ.

LaTeX

$$$$ \\mathrm{GoodProducts}.\\mathrm{eval}\\ C\\ l : \\mathrm{LocallyConstant}\\ C\\mathbb{Z}. $$$$

Lean4

/-- Evaluation of good products. -/
def eval (l : { l : Products I // l.isGood C }) : LocallyConstant C ℤ :=
  Products.eval C l.1

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

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

Разделы

Аффилиация

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