English
For a family of lattices (α_i) indexed by i in I, the evaluation map at i sends a function f: I → α_i to its i-th value f(i). This evaluation is a lattice homomorphism from the function space to α_i.
Русский
Для семейства решеток (α_i), индексируемого I, отображение оценки в точке i отправляет функцию f: I → α_i в значение f(i) и является гомоморфизмом решетки.
LaTeX
$$$\\operatorname{evalLatticeHom}(i): \\bigl(\\forall i, \\alpha_i\\bigr) \\to \\alpha_i\\quad\\text{with}\\quad \\operatorname{toFun}(\\operatorname{evalLatticeHom}(i)) = \\operatorname{Function.eval}_i$$$
Lean4
/-- Evaluation as a lattice homomorphism. -/
def evalLatticeHom (i : ι) : LatticeHom (∀ i, α i) (α i)
where
toFun := Function.eval i
map_sup' _a _b := rfl
map_inf' _a _b := rfl
