cons_eta — Mathlib

English

For any f defined on i :: l, the Pi-construction with head and tail recovers f: List.Pi.cons i l (List.Pi.head f) (List.Pi.tail f) = f.

Русский

Для любой функции f, определённой на i :: l, конструкция Pi с головой и хвостом восстанавливает f: List.Pi.cons i l (List.Pi.head f) (List.Pi.tail f) = f.

LaTeX

$$$\text{List.Pi.cons } i \; l \; (\text{List.Pi.head } f) \; (\text{List.Pi.tail } f) = f$$$

Lean4

@[simp]
theorem cons_eta (f : ∀ j ∈ i :: l, α j) : cons _ _ (head f) (tail f) = f :=
  Multiset.Pi.cons_eta (α := ι) (m := l) f

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