Theorems · Theorem · probability
MeasureTheory.Filtration.mono
∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {i j : ι}
(f : MeasureTheory.Filtration ι m), i ≤ j → ↑f i ≤ ↑f j- Defined in
- Mathlib.Probability.Process.Filtration
- Cited by
- 39 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext, Quot.sound
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- Preorderstatement and proof · cited by 7,952
- MeasureTheory.Filtrationstatement and proof · cited by 425
- MeasureTheory.Filtration.seqstatement · cited by 184
- MeasureTheory.Filtration.mono'proof · cited by 1
Cited by39
Results whose statement or proof uses this declaration.
- MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iffproof · cited by 6
- MeasureTheory.Adapted.isStoppingTime_hittingBtwnproof · cited by 5
- MeasureTheory.IsStoppingTime.measurableSet_le'proof · cited by 5
- MeasureTheory.IsStoppingTime.measurableSet_eq_of_countable_rangeproof · cited by 4
- MeasureTheory.StronglyAdapted.isStronglyProgressive_of_continuousproof · cited by 4
- MeasureTheory.IsStoppingTime.measurableSpace_constproof · cited by 4
- MeasureTheory.IsStronglyPredictable.of_measurable_add_oneproof · cited by 4
- MeasureTheory.Filtration.condExp_condExpproof · cited by 3
- MeasureTheory.martingale_martingalePartproof · cited by 2
- ProbabilityTheory.Kernel.setIntegral_densityproof · cited by 2
- ProbabilityTheory.Kernel.setIntegral_densityProcess_of_leproof · cited by 2
- MeasureTheory.isStronglyProgressive_min_stopping_timeproof · cited by 2