English
There is a natural equivalence between the dependent function type ∀ i, β i and the product of the two restricted pi-types: (∀ i, β i) ≃ (∀ i : {x | p x}, β i) × ∀ i : {x | ¬p x}, β i.
Русский
Существует естественная эквиваленция между зависимым типом функций ∀ i, β i и произведением двух ограниченных по подтипам п-типов: (∀ i, β i) ≃ (∀ i ∈ {x | p x}, β i) × ∀ i ∈ {x | ¬p x}, β i.
LaTeX
$$$\big(\forall i:\alpha, \beta(i)\big) \simeq \Big(\forall i : \{ x \mid p x \}, \beta(i)\Big) \times \Big(\forall i : \{ x \mid \neg p x \}, \beta(i)\Big).$$$
Lean4
/-- The type `∀ (i : α), β i` can be split as a product by separating the indices in `α`
depending on whether they satisfy a predicate `p` or not. -/
@[simps]
def piEquivPiSubtypeProd {α : Type*} (p : α → Prop) (β : α → Type*) [DecidablePred p] :
(∀ i : α, β i) ≃ (∀ i : { x // p x }, β i) × ∀ i : { x // ¬p x }, β i
where
toFun f := (fun x => f x, fun x => f x)
invFun f x := if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩
right_inv := by
rintro ⟨f, g⟩
ext1 <;> grind
left_inv f := by grind
