piOptionEquivProd — Mathlib

English

The forward map of sumPiEquivProdPi α is measurable and its inverse is measurable, yielding a measurable equivalence.

Русский

Прямая карта sumPiEquivProdPi α измерима, как и её обратная карта, что дает измеримую эквивалентность.

LaTeX

$$$ \\text{Measurable} \\big( \\mathrm{toFun}(\\mathrm{Equiv.sumPiEquivProdPi}\\alpha) \\big) \\land \\text{Measurable}( \\mathrm{toFun}(\\mathrm{Equiv.sumPiEquivProdPi}\\alpha)^{-1}) $$$

Lean4

/-- The measurable equivalence for (dependent) functions on an Option type
  `(∀ i : Option δ, α i) ≃ᵐ (∀ (i : δ), α i) × α none`. -/
def piOptionEquivProd {δ : Type*} (α : Option δ → Type*) [∀ i, MeasurableSpace (α i)] :
    (∀ i, α i) ≃ᵐ (∀ (i : δ), α i) × α none :=
  let e : Option δ ≃ δ ⊕ Unit := Equiv.optionEquivSumPUnit δ
  let em1 : ((i : δ ⊕ Unit) → α (e.symm i)) ≃ᵐ ((a : Option δ) → α a) := MeasurableEquiv.piCongrLeft α e.symm
  let em2 :
    ((i : δ ⊕ Unit) → α (e.symm i)) ≃ᵐ ((i : δ) → α (e.symm (Sum.inl i))) × ((i' : Unit) → α (e.symm (Sum.inr i'))) :=
    MeasurableEquiv.sumPiEquivProdPi (fun i ↦ α (e.symm i))
  let em3 :
    ((i : δ) → α (e.symm (Sum.inl i))) × ((i' : Unit) → α (e.symm (Sum.inr i'))) ≃ᵐ ((i : δ) → α (some i)) × α none :=
    MeasurableEquiv.prodCongr (MeasurableEquiv.refl ((i : δ) → α (e.symm (Sum.inl i))))
      (MeasurableEquiv.piUnique fun i ↦ α (e.symm (Sum.inr i)))
  em1.symm.trans <| em2.trans em3

Похожие утверждения