English
A natural homeomorphism between the dependent product over ι and the product over subtypes induced by a predicate p.
Русский
Естественный гомеоморфизм зависимого произведения над ι и произведения по подтипам, заданного предикатом p.
LaTeX
$$$ {\iota : Type}\, p:\iota → Prop,\ Y:\iota → Type,\ [∀ i, TopologicalSpace (Y i)], \text{Homeomorph} ((i:\iota) → Y i) \nobreak\to ((i : {x // p x}) → Y i.x) × ((i : {x // Not (p x)}) → Y i.x).$$$
Lean4
/-- The topological space `Π i, Y 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 (p : ι → Prop) (Y : ι → Type*) [∀ i, TopologicalSpace (Y i)] [DecidablePred p] :
(∀ i, Y i) ≃ₜ (∀ i : { x // p x }, Y i) × ∀ i : { x // ¬p x }, Y i
where
toEquiv := Equiv.piEquivPiSubtypeProd p Y
continuous_toFun := by apply Continuous.prodMk <;> exact continuous_pi fun j => continuous_apply j.1
continuous_invFun :=
continuous_pi fun j => by
dsimp only [Equiv.piEquivPiSubtypeProd]; split_ifs
exacts [(continuous_apply _).comp continuous_fst, (continuous_apply _).comp continuous_snd]
