Theorems · Definition · probability
MeasurableEquiv.piSingleton
{X : ℕ → Type u_1} →
[inst : (n : ℕ) → MeasurableSpace (X n)] → (a : ℕ) → X (a + 1) ≃ᵐ ((i : ↥(Finset.Ioc a (a + 1))) → X ↑i)Identifying {a + 1} with Ioc a (a + 1), as a measurable equiv on dependent functions.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- MeasurableSpacestatement and proof · cited by 13,106
- Finset.Iocstatement and proof · cited by 301
- MeasurableEquivstatement · cited by 269
Cited by11
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.partialTrajproof · cited by 44
- ProbabilityTheory.Kernel.partialTraj_succ_selfstatement and proof · cited by 6
- ProbabilityTheory.Kernel.partialTraj_succ_of_lestatement and proof · cited by 3
- ProbabilityTheory.Kernel.partialTraj_eq_prodproof · cited by 3
- ProbabilityTheory.Kernel.partialTraj_succ_eq_compproof · cited by 2
- MeasureTheory.partialTraj_const_restrict₂proof · cited by 1
- ProbabilityTheory.Kernel.partialTraj_succ_map_frestrictLe₂proof · cited by 1
- ProbabilityTheory.Kernel.map_partialTraj_succ_selfproof · cited by 1
- MeasureTheory.Measure.map_piSingletonstatement and proof · cited by 1
- ProbabilityTheory.Kernel.lmarginalPartialTraj_succproof · cited by 1
- ProbabilityTheory.Kernel.partialTraj_le_defstatement and proof · cited by 1