English
There is a canonical way to extend a family of types f i by inserting a at position a into a finite index set s, turning a pair (f a, ∏ i∈s, f i) into a product over insert a s, i.e., a canonical map prodPiInsert that defines the i-th coordinate depending on whether i equals a or lies in s.
Русский
Существует канонический способ расширить семейство типов f i путем вставки индекса a в множество s, переводящий пару (f a, ∏ i∈s, f i) в произведение над insert a s; определена явная карта prodPiInsert.
LaTeX
$$$\\text{prodPiInsert} : f a \\times \\prod_{i\\in s} f i \\to \\prod_{i\\in \\operatorname{insert} a s} f i,$ with $(\\text{prodPiInsert} f x)(i) = \\begin{cases} x_1 \\text{ if } i=a, \\\\ x_2(i) \\text{ if } i\\in s. \\end{cases}$$$
Lean4
/-- Split the added element of insert off a Pi type. -/
@[simps!]
def insertPiProd (f : α → Type*) (x : Π i ∈ insert a s, f i) : f a × Π i ∈ s, f i :=
(x a (mem_insert_self a s), fun i hi => x i (mem_insert_of_mem hi))
