English
There is a canonical equivalence between the pi-type over insert a s and the product f a × (pi-type over s) whenever a ∉ s; this equivalence is given by insertPiProdEquiv with explicit forward and backward directions using insertPiProd and prodPiInsert.
Русский
Существует каноническая эквиваленция между Pi-типом над insert a s и произведением f a × (Pi над s), когда a не принадлежит s; эквиваленция задаётся insertPiProdEquiv через insertPiProd и prodPiInsert.
LaTeX
$$$\\operatorname{insertPiProdEquiv} : (\\Pi i \\in \\operatorname{insert} a s, f i) \\simeq f a \\times \\Pi i \\in s, f i$ (при $a \\notin s$).$$
Lean4
/-- The equivalence between pi types on insert and the product. -/
def insertPiProdEquiv [DecidableEq α] {s : Finset α} (f : α → Type*) {a : α} (has : a ∉ s) :
(Π i ∈ insert a s, f i) ≃ f a × Π i ∈ s, f i
where
toFun := insertPiProd f
invFun := prodPiInsert f
left_inv _ := by grind [prodPiInsert, insertPiProd]
right_inv
_ := by
ext _ hi <;>
grind [prodPiInsert, insertPiProd]
-- useful rules for calculations with quantifiers
