coe_evalLatticeHom

Mathlib.Order.Hom.Lattice

URI: https://scilib.ai/kg/mathlib#Pi.coe_evalLatticeHom

English

For each i, the underlying function of evalLatticeHom i coincides with the evaluation function at i.

Русский

Для каждого i базовая функция evalLatticeHom i совпадает с функцией оценки в i.

LaTeX

$$$\\operatorname{coev}(\\operatorname{evalLatticeHom}(i)) = \\operatorname{Function.eval}_i$$$

Lean4

@[simp, norm_cast]
theorem coe_evalLatticeHom (i : ι) : ⇑(evalLatticeHom (α := α) i) = Function.eval i :=
  rfl

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

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

Разделы

Аффилиация

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