Theorems · Theorem · probability
MeasureTheory.measurableSet_prodMk_add_one_of_predictable
∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ℕ m} {s : Set (ℕ × Ω)},
MeasurableSet s → ∀ (n : ℕ), MeasurableSet {ω | (n + 1, ω) ∈ s}- Defined in
- Mathlib.Probability.Process.Predictable
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites24
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- MeasurableSpacestatement and proof · cited by 13,106
- Set.Elemproof · cited by 7,166
- Set.ofPredstatement and proof · cited by 6,101
- Bot.botproof · cited by 4,720
- MeasurableSetstatement and proof · cited by 3,075
- Set.extproof · cited by 2,266
- SProd.sprodproof · cited by 1,750
- Set.Ioiproof · cited by 1,463
- MeasureTheory.Filtrationstatement and proof · cited by 425
- MeasureTheory.Filtration.seqstatement · cited by 184
- lt_or_geproof · cited by 182
Cited by1
Results whose statement or proof uses this declaration.
- MeasureTheory.IsStronglyPredictable.measurable_add_oneproof · cited by 6