English
From a pair (f a, Π i∈s, f i) build a function on cons a s, by choosing the value at a for i=a and using the rest for i∈s.
Русский
Из пары (f(a), Π i∈s, f(i)) строится функция на объединении a вместе с s: для i=a берём значение из f(a), для i∈s — из второй компоненты.
LaTeX
$$$\text{prodPiCons} : (f a \times Π i ∈ s, f i) \to (Π i ∈ \operatorname{cons}(a,s,has), f i)$ с определением: $g(a,ha)=x.1$ и $g(i,mem) = x.2 i mem$.$$
Lean4
/-- Combine a product with a pi type to pi of cons. -/
def prodPiCons [DecidableEq α] (f : α → Type*) {a : α} (has : a ∉ s) (x : f a × Π i ∈ s, f i) :
(Π i ∈ cons a s has, f i) := fun i hi =>
if h : i = a then cast (congrArg f h.symm) x.1 else x.2 i (mem_of_mem_cons_of_ne hi h)
