ProbabilityTheory.Kernel.MeasurableEquiv.IicSuccProd_apply🔗

This page has the declaration's own card below, then its dependency graph, then a card for each dependency (type dependencies first, then the rest of the transitive closure). For a theorem, the graph and the dependency cards only follow its statement's dependencies (its proof is replaced by sorry, so what it proves doesn't depend on how); for everything else, both the type and the body/value are followed, since their content is part of what later declarations build on.

Minimal Lean file

ProbabilityTheory.Kernel.MeasurableEquiv.IicSuccProd_apply.{u_2}
  {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ)
  (h : (i : ↥(Finset.Iic (n + 1))) → X ↑i) :
  (MeasurableEquiv.IicSuccProd X n) h =
    (fun i => h ⟨↑i, ⋯⟩, h ⟨n + 1, ⋯⟩)
ProbabilityTheory.Kernel.MeasurableEquiv.IicSuccProd_apply.{u_2}
  {X : ℕ → Type u_2}
  [(n : ℕ) → MeasurableSpace (X n)]
  (n : ℕ)
  (h :
    (i : ↥(Finset.Iic (n + 1))) → X ↑i) :
  (MeasurableEquiv.IicSuccProd X n) h =
    (fun i => h ⟨↑i, ⋯⟩, h ⟨n + 1, ⋯⟩)

lemma MeasurableEquiv.IicSuccProd_apply (n : ℕ) (h : Π i : Iic (n + 1), X i) :
    MeasurableEquiv.IicSuccProd X n h = (fun i : Iic n ↦ h ⟨i.1, by grind⟩, h ⟨n + 1, by simp⟩)

rfl

Dependency graph

Type dependencies (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)

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)