Theorems · Theorem · probability

MeasureTheory.IsStoppingTime.measurableSpace_min

∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ π : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) (hπ : MeasureTheory.IsStoppingTime f π),
  ⋯.measurableSpace = hτ.measurableSpace ⊓ hπ.measurableSpace

Defined in: Mathlib.Probability.Process.Stopping
Cited by: 4 results in Mathlib
Foundations: Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: LinearOrder

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setproof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
LinearOrderstatement and proof · cited by 8,572
Set.ofPredproof · cited by 6,101
WithTopstatement and proof · cited by 3,754
MeasurableSetproof · cited by 3,075
Set.extproof · cited by 2,266
le_antisymmproof · cited by 2,068
WithTop.someproof · cited by 1,128
MeasureTheory.Filtrationstatement and proof · cited by 425
MeasureTheory.IsStoppingTimestatement and proof · cited by 122
le_infproof · cited by 107

Cited by4

Results whose statement or proof uses this declaration.

MeasureTheory.IsStoppingTime.measurableSet_min_iffproof · cited by 5
MeasureTheory.IsStoppingTime.measurableSpace_min_constproof · cited by 2
MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_leproof · cited by 1
MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExpproof · cited by 0