Theorems · Theorem · probability

MeasureTheory.IsStoppingTime.iInf

∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrderBot ι]
  [inst_1 : TopologicalSpace ι] [OrderTopology ι] [DenselyOrdered ι] [FirstCountableTopology ι] [NoMaxOrder ι]
  {κ : Type u_4} [Countable κ] {f : MeasureTheory.Filtration ι m} {τ : κ → Ω → WithTop ι} [f.IsRightContinuous],
  (∀ (n : κ), MeasureTheory.IsStoppingTime f (τ n)) → MeasureTheory.IsStoppingTime f fun ω => ⨅ n, τ n ω

Defined in: Mathlib.Probability.Process.Stopping
Cited by: 0 results in Mathlib
Foundations: Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: ConditionallyCompleteLinearOrderBot TopologicalSpace OrderTopology DenselyOrdered FirstCountableTopology NoMaxOrder Countable MeasureTheory.Filtration.IsRightContinuous

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.

TopologicalSpacestatement and proof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
Preorderproof · cited by 7,952
Set.univproof · cited by 3,945
WithTopstatement and proof · cited by 3,754
iInfstatement and proof · cited by 1,690
OrderTopologystatement and proof · cited by 1,355
Countablestatement and proof · cited by 633
DenselyOrderedstatement and proof · cited by 471
MeasureTheory.Filtrationstatement and proof · cited by 425
NoMaxOrderstatement and proof · cited by 340
iInf_congr_Propproof · cited by 218

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.