English
There is a measurable equivalence between dependent functions on an option type and a pair consisting of functions on δ and a function at none.
Русский
Существует измеримая эквивалентность между зависящими функциями на типе Option и парой функций: по δ и по none.
LaTeX
$$$ (\\forall i:\\mathrm{Option}\\, \\delta, \\pi i) \\simeq^m (\\forall i:\\delta, \\pi(\\mathrm{Option.some}\, i)) \\times (\\alpha\\mathrm{none}) $$$
Lean4
/-- If `s` is a measurable set in a measurable space, that space is equivalent
to the sum of `s` and `sᶜ`. -/
def sumCompl {s : Set α} [DecidablePred (· ∈ s)] (hs : MeasurableSet s) : s ⊕ (sᶜ : Set α) ≃ᵐ α
where
toEquiv := .sumCompl (· ∈ s)
measurable_toFun := measurable_subtype_coe.sumElim measurable_subtype_coe
measurable_invFun := Measurable.dite measurable_inl measurable_inr hs
