English
There is a canonical equivalence between the Pi-type over cons a s and the product f a × ∏ i∈s, f i, given a ∉ s.
Русский
Существует каноническая эквивалентность между зависимым произведением над объединением cons(a,s) и произведением f(a) × ∏_{i∈s} f(i), при условии a ∉ s.
LaTeX
$$$\text{consPiProdEquiv} : (Π i ∈ \operatorname{cons}(a,s,has), f i) \simeq f(a) \times (Π i ∈ s, f i)$$$
Lean4
/-- The equivalence between pi types on cons and the product. -/
def consPiProdEquiv [DecidableEq α] {s : Finset α} (f : α → Type*) {a : α} (has : a ∉ s) :
(Π i ∈ cons a s has, f i) ≃ f a × Π i ∈ s, f i
where
toFun := consPiProd f has
invFun := prodPiCons f has
left_inv _ := by grind [prodPiCons, consPiProd]
right_inv
_ := by
-- I'm surprised `grind` needs this `ext` step: it is just `Prod.ext` and `funext`.
ext _ hi <;> grind [prodPiCons, consPiProd]
