evalLatticeHom_apply

Mathlib.Order.Hom.Lattice

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

English

For every index i, applying evalLatticeHom i to a function f yields its value at i: evalLatticeHom i (f) = f(i).

Русский

Для каждого индекса i применение evalLatticeHom i к функции f даёт значение f в i: evalLatticeHom i (f) = f(i).

LaTeX

$$$\\forall i,\\; \\operatorname{evalLatticeHom}(i)(f) = f(i)$$$

Lean4

theorem evalLatticeHom_apply (i : ι) (f : ∀ i, α i) : evalLatticeHom i f = f i :=
  rfl

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

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

Разделы

Аффилиация

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