English
There is a measurable equivalence between dependent functions (i ↦ π i) and the pair consisting of functions on the subtype {i | p i} and on the complement {i | ¬p i}. This is a measurable version of pi-equivalences for subtypes.
Русский
Существует измеримая эквивалентность между зависящими функциями (i ↦ π i) и парой функций на подтипе {i | p i} и на комплементе {i | ¬p i}. Это измеримая версия pi-эквивалентности для подтипов.
LaTeX
$$$ (\\forall i, \\pi(i)) \\simeq^m (\\forall i:\\mathrm{Subtype}\\ p, \\pi(i)) \\times (\\forall i:\\{i\\,|\\,\\neg p i\\}, \\pi(i)) $$$
Lean4
/-- Measurable equivalence between (dependent) functions on a type and pairs of functions on
`{i // p i}` and `{i // ¬p i}`. See also `Equiv.piEquivPiSubtypeProd`. -/
@[simps! -fullyApplied]
def piEquivPiSubtypeProd (p : δ' → Prop) [DecidablePred p] :
(∀ i, π i) ≃ᵐ (∀ i : Subtype p, π i) × ∀ i : { i // ¬p i }, π i
where
toEquiv := .piEquivPiSubtypeProd p π
measurable_toFun := measurable_piEquivPiSubtypeProd π p
measurable_invFun := measurable_piEquivPiSubtypeProd_symm π p
