evalCons — Mathlib

English

Evaluation on a cons-list satisfies a recursive multiplication by e C a with tail evaluation.

Русский

Оценивание конструкторной последовательности удовлетворяет рекурсивному умножению на e C a и оценке хвоста.

LaTeX

$$$\\mathrm{Products.eval}\\ C (\\langle a :: l, \\text{hla}\\rangle) = e\\ C\\ a \\cdot \\mathrm{Products.eval}\\ C (\\langle l, \\cdots \\rangle)$$$

Lean4

theorem evalCons {I} [LinearOrder I] {C : Set (I → Bool)} {l : List I} {a : I} (hla : (a :: l).IsChain (· > ·)) :
    Products.eval C ⟨a :: l, hla⟩ =
      (e C a) * Products.eval C ⟨l, List.IsChain.sublist hla (List.tail_sublist (a :: l))⟩ :=
  by simp only [eval.eq_1, List.map, List.prod_cons]

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