Theorems · Theorem · probability

MeasureTheory.IsStoppingTime.add

∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Add ι] [inst_1 : LinearOrder ι]
  [CanonicallyOrderedAdd ι] [Countable ι] [inst_4 : TopologicalSpace ι] [OrderTopology ι]
  {f : MeasureTheory.Filtration ι m} {τ π : Ω → WithTop ι},
  MeasureTheory.IsStoppingTime f τ → MeasureTheory.IsStoppingTime f π → MeasureTheory.IsStoppingTime f (τ + π)

Defined in: Mathlib.Probability.Process.Stopping
Cited by: 0 results in Mathlib
Foundations: Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Add LinearOrder CanonicallyOrderedAdd Countable TopologicalSpace OrderTopology

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites23

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
Top.topproof · cited by 9,680
LinearOrderstatement and proof · cited by 8,572
Set.Elemproof · cited by 7,166
Set.ofPredproof · cited by 6,101
WithTopstatement and proof · cited by 3,754
Set.iUnionproof · cited by 2,483
Set.extproof · cited by 2,266
OrderTopologystatement and proof · cited by 1,355
WithTop.someproof · cited by 1,128
Set.Iicproof · cited by 1,111

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.