Theorems · Theorem · probability
MeasureTheory.IsStoppingTime.measurableSet_min_iff
∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
{τ π : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) (hπ : MeasureTheory.IsStoppingTime f π) (s : Set Ω),
MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s- Defined in
- Mathlib.Probability.Process.Stopping
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LinearOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
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
- LinearOrderstatement and proof · cited by 8,572
- WithTopstatement and proof · cited by 3,754
- MeasurableSetstatement and proof · cited by 3,075
- MeasureTheory.Filtrationstatement and proof · cited by 425
- MeasureTheory.IsStoppingTimestatement and proof · cited by 122
- MeasureTheory.IsStoppingTime.measurableSpacestatement · cited by 49
- MeasureTheory.IsStoppingTime.minstatement · cited by 12
- MeasureTheory.IsStoppingTime.measurableSpace_minproof · cited by 4
Cited by5
Results whose statement or proof uses this declaration.
- MeasureTheory.IsStoppingTime.measurableSet_inter_le_iffproof · cited by 3
- MeasureTheory.IsStoppingTime.measurableSet_inter_le_const_iffproof · cited by 1
- MeasureTheory.IsStoppingTime.measurableSet_stopping_time_leproof · cited by 1
- MeasureTheory.IsStoppingTime.measurableSet_eq_stopping_timeproof · cited by 0