English
Let l be an element of MaxProducts for C with parameter ho. Then applying the linear operator Linear_CC'(C, hsC, ho) to the value l.val.eval C yields the same result as evaluating the tail l.val.Tail under the modified family C' C ho.
Русский
Пусть l — элемент множества MaxProducts для C с параметром ho. Тогда применение линейного оператора Linear_CC'(C, hsC, ho) к значению l.val.eval C даёт тот же результат, что и вычисление хвоста l.val.Tail через модифицированную семью C' C ho.
LaTeX
$$$\mathrm{Linear\_CC'}(C,hsC,ho)\bigl(l.\mathrm{val}.\mathrm{eval}\, C\bigr) = l.\mathrm{val}.\mathrm Tail.\mathrm{eval}(C'\, C\, ho)$$$
Lean4
theorem max_eq_eval (l : MaxProducts C ho) : Linear_CC' C hsC ho (l.val.eval C) = l.val.Tail.eval (C' C ho) :=
have : Inhabited I := ⟨term I ho⟩
Products.max_eq_eval _ _ _ _ (List.ne_nil_of_mem l.prop.2) (head!_eq_o_of_maxProducts _ hsC ho l)
