piFinsetUnion — Mathlib

English

One of the proofs asserts the measurability of the forward component of sumPiEquivProdPi α.

Русский

Один из доказательств утверждает измеримость прямой компоненты sumPiEquivProdPi α.

LaTeX

$$$ \\mathrm{Measurable} (\\mathrm{toFun}(\\mathrm{Equiv.sumPiEquivProdPi}\\alpha)) $$$

Lean4

/-- The measurable equivalence `(∀ i : s, π i) × (∀ i : t, π i) ≃ᵐ (∀ i : s ∪ t, π i)`
  for disjoint finsets `s` and `t`. `Equiv.piFinsetUnion` as a measurable equivalence. -/
def piFinsetUnion [DecidableEq δ'] {s t : Finset δ'} (h : Disjoint s t) :
    ((∀ i : s, π i) × ∀ i : t, π i) ≃ᵐ ∀ i : (s ∪ t : Finset δ'), π i :=
  letI e := Finset.union s t h
  MeasurableEquiv.sumPiEquivProdPi (fun b ↦ π (e b)) |>.symm.trans <| .piCongrLeft (fun i : ↥(s ∪ t) ↦ π i) e

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