Theorems · Theorem · probability
MeasureTheory.Filtration.rightCont_eq_of_not_isMax
∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : LinearOrder ι] [DenselyOrdered ι]
(𝓕 : MeasureTheory.Filtration ι m) {i : ι}, ¬IsMax i → ↑𝓕.rightCont i = ⨅ j, ⨅ (_ : j > i), ↑𝓕 j- Defined in
- Mathlib.Probability.Process.Filtration
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LinearOrderDenselyOrdered
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpaceproof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- LinearOrderstatement and proof · cited by 8,572
- nhdsWithinproof · cited by 1,912
- iInfstatement · cited by 1,690
- Set.Ioiproof · cited by 1,463
- OrderTopologyproof · cited by 1,355
- Filter.NeBotproof · cited by 853
- DenselyOrderedstatement and proof · cited by 471
- MeasureTheory.Filtrationstatement and proof · cited by 425
- IsMaxstatement and proof · cited by 372
- MeasureTheory.Filtration.seqstatement · cited by 184
Cited by1
Results whose statement or proof uses this declaration.
- MeasureTheory.Filtration.rightCont_eqproof · cited by 0