max_eq_eval_unapply — Mathlib

English

Let C be a closed subset of Bool-valued functions on I with a linear order. Then the evaluation map on maximal products factors through the tail evaluation under the restricted set C'.

Русский

Пусть C замкнутое множество функций вида I → Bool. Тогда отображение оценки на максимальных произведениях факторизуется через оценку хвоста при ограниченном множестве C'.

LaTeX

$$$\\big( \\mathrm{Linear\\_CC'}\\;C\\;h_s\\;h_o \\right) \\circ \\big( \\lambda l. \\mathrm{Products.eval}\\;C\\;l.\\mathrm{val} \\big) = \\big( \\lambda l. l.\\mathrm{val}.\\mathrm{Tail}.\\mathrm{eval}(C'\\,C\\;h_o) \\big)$$$

Lean4

theorem max_eq_eval_unapply :
    (Linear_CC' C hsC ho) ∘ (fun (l : MaxProducts C ho) ↦ Products.eval C l.val) =
      (fun l ↦ l.val.Tail.eval (C' C ho)) :=
  by
  ext1 l
  exact max_eq_eval _ _ _ _

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