English
The Pi-cons operation commutes with a pointwise map: applying φ to the head and the tail maps is the same as mapping φ over the Pi-construction.
Русский
Операция конструирования Pi-компонента коммутирует с композицией: применение φ ко всем компонентам эквивалентно отображению φ по Pi-конструкции.
LaTeX
$$$\text{cons } i l (\phi a) (\lambda j \; hj \; \mapsto \phi (f j hj)) = (\lambda j \; hj \; \mapsto \phi ((\text{cons } i l a f) j hj))$$$
Lean4
theorem cons_map (a : α i) (f : ∀ j ∈ l, α j) {α' : ι → Sort*} (φ : ∀ ⦃j⦄, α j → α' j) :
cons _ _ (φ a) (fun j hj ↦ φ (f j hj)) = (fun j hj ↦ φ ((cons _ _ a f) j hj)) :=
Multiset.Pi.cons_map _ _ _
