Measurable equivalence between a product up to n + 1 and the pair of the product up to n and the space at n + 1.

MeasurableEquiv.IicSuccProd.{u_3} (X : ℕ → Type u_3)
  [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) :
  ((i : ↥(Finset.Iic (n + 1))) → X ↑i) ≃ᵐ
    ((i : ↥(Finset.Iic n)) → X ↑i) × X (n + 1)
MeasurableEquiv.IicSuccProd.{u_3}
  (X : ℕ → Type u_3)
  [(n : ℕ) → MeasurableSpace (X n)]
  (n : ℕ) :
  ((i : ↥(Finset.Iic (n + 1))) → X ↑i) ≃ᵐ
    ((i : ↥(Finset.Iic n)) → X ↑i) ×
      X (n + 1)

Code

def _root_.MeasurableEquiv.IicSuccProd (X : ℕ → Type*) [∀ n, MeasurableSpace (X n)] (n : ℕ) :
    MeasurableEquiv (Π i : Iic (n + 1), X i) ((Π i : Iic n, X i) × X (n + 1)) :=
  (MeasurableEquiv.IicProdIoc (Nat.le_succ n)).symm.trans
    (MeasurableEquiv.prodCongr (MeasurableEquiv.refl _) (MeasurableEquiv.piSingleton n).symm)

Actions: Source · Open Issue