English
For a fixed index i in α, the product type ∀ j, β j splits as β i × ∀ j ≠ i, β j, via choosing the i-th slot and the rest.
Русский
Для фиксированного индекса i в α произведение типов ∀ j, β j распадается на β i × ∀ j ≠ i, β j, выбирая i-ю компоненту и остаток.
LaTeX
$$$\text{Equiv} (\forall j, \beta(j)) \simeq \beta(i) \times (\forall j : \{ j \neq i \}, \beta(j)).$$$
Lean4
/-- A product of types can be split as the binary product of one of the types and the product
of all the remaining types. -/
@[simps]
def piSplitAt {α : Type*} [DecidableEq α] (i : α) (β : α → Type*) : (∀ j, β j) ≃ β i × ∀ j : { j // j ≠ i }, β j
where
toFun f := ⟨f i, fun j => f j⟩
invFun f j := if h : j = i then h.symm.rec f.1 else f.2 ⟨j, h⟩
right_inv f := by ext x <;> grind
left_inv f := by grind
