English
If a is not in s, the two dependent products over insert a s and over s are canonically isomorphic: Π i∈insert a s, f i ≃ f a × Π i∈s, f i. The isomorphism is given by insertPiProd and its inverse by prodPiInsert, with the inverses characterized by the simple coherence conditions.
Русский
Пусть a не принадлежит s. Т эти зависимые произведения над insert a s и над s канонически изоморфны: Π i∈insert a s, f i ≃ f a × Π i∈s, f i. Изоморфизм задаётся insertPiProd и обратное отображение prodPiInsert, удовлетворяющее условиям обратимости.
LaTeX
$$$\\bigl(\\Pi i \\in \\operatorname{insert} a s,\n f i\\bigr) \\simeq f a \\times \\bigl(\\Pi i \\in s, f i\\bigr),$ при $a \\notin s$.$$
Lean4
/-- Combine a product with a pi type to pi of insert. -/
def prodPiInsert (f : α → Type*) {a : α} (x : f a × Π i ∈ s, f i) : (Π i ∈ insert a s, f i) := fun i hi =>
if h : i = a then cast (congrArg f h.symm) x.1 else x.2 i (mem_of_mem_insert_of_ne hi h)
