English
For any l in the good product family, and x in C, the evaluation l.eval C x equals 1 if and only if x(i) = true for every i in the support l.val; otherwise it equals 0.
Русский
Для любого l из семейства хороших продуктов и для любого x из C, значение l.eval C x равно 1 тогда и только тогда, когда для каждого i в поддержке l.val x(i) = true; иначе равно 0.
LaTeX
$$$l.\\mathrm{eval}(C)\,x = \\begin{cases} 1, & \\text{если } \\forall i,\\ i \\in l.\\mathrm{val} \\Rightarrow x(i)=\\text{true}, \\\\ 0, & \\text{иначе}. \\end{cases}$$$
Lean4
theorem eval_eq (l : Products I) (x : C) : l.eval C x = if ∀ i, i ∈ l.val → (x.val i = true) then 1 else 0 :=
by
change LocallyConstant.evalMonoidHom x (l.eval C) = _
rw [eval, map_list_prod]
split_ifs with h
· simp only [List.map_map]
apply List.prod_eq_one
simp only [List.mem_map, Function.comp_apply]
rintro _ ⟨i, hi, rfl⟩
exact if_pos (h i hi)
· simp only [List.map_map, List.prod_eq_zero_iff, List.mem_map, Function.comp_apply]
push_neg at h
convert h with i
dsimp [LocallyConstant.evalMonoidHom, e]
simp only [ite_eq_right_iff, one_ne_zero]
