Stopping

📁 Source: Mathlib/Probability/Process/Stopping.lean

Statistics

Metric	Count
Definitions `IsStoppingTime`, `measurableSpace`, `stoppedProcess`, `stoppedValue`	4
Theorems `add`, `add_const`, `add_const'`, `le_measurableSpace_of_const_le`, `max`, `max_const`, `measurable`, `measurable'`, `measurableSet`, `measurableSet_eq`, `measurableSet_eq'`, `measurableSet_eq_le`, `measurableSet_eq_of_countable`, `measurableSet_eq_of_countable'`, `measurableSet_eq_of_countable_range`, `measurableSet_eq_of_countable_range'`, `measurableSet_eq_stopping_time`, `measurableSet_eq_stopping_time_min`, `measurableSet_eq_stopping_time_of_countable`, `measurableSet_eq_top`, `measurableSet_ge`, `measurableSet_ge'`, `measurableSet_ge_of_countable`, `measurableSet_ge_of_countable'`, `measurableSet_ge_of_countable_range`, `measurableSet_ge_of_countable_range'`, `measurableSet_gt`, `measurableSet_gt'`, `measurableSet_inter_eq_iff`, `measurableSet_inter_le`, `measurableSet_inter_le_const_iff`, `measurableSet_inter_le_iff`, `measurableSet_le`, `measurableSet_le'`, `measurableSet_le_stopping_time`, `measurableSet_lt`, `measurableSet_lt'`, `measurableSet_lt_le`, `measurableSet_lt_of_countable`, `measurableSet_lt_of_countable'`, `measurableSet_lt_of_countable_range`, `measurableSet_lt_of_countable_range'`, `measurableSet_lt_of_isLUB`, `measurableSet_lt_of_pred`, `measurableSet_min_const_iff`, `measurableSet_min_iff`, `measurableSet_stopping_time_le`, `measurableSet_stopping_time_le_min`, `measurableSpace_const`, `measurableSpace_le`, `measurableSpace_le_of_countable`, `measurableSpace_le_of_countable_range`, `measurableSpace_le_of_le`, `measurableSpace_le_of_le_const`, `measurableSpace_min`, `measurableSpace_min_const`, `measurableSpace_mono`, `measurable_of_le`, `min`, `min_const`, `piecewise_of_le`, `sigmaFinite_stopping_time`, `sigmaFinite_stopping_time_of_le`, `stoppedProcess`, `stronglyAdapted_stoppedProcess`, `stronglyMeasurable_stoppedProcess`, `stoppedProcess`, `stoppedProcess_of_discrete`, `stronglyMeasurable_stoppedProcess`, `stronglyMeasurable_stoppedProcess_of_discrete`, `condExp_min_stopping_time_ae_eq_restrict_le`, `condExp_min_stopping_time_ae_eq_restrict_le_const`, `condExp_stopping_time_ae_eq_restrict_eq`, `condExp_stopping_time_ae_eq_restrict_eq_of_countable`, `condExp_stopping_time_ae_eq_restrict_eq_of_countable_range`, `integrable_stoppedProcess`, `integrable_stoppedProcess_of_mem_finset`, `integrable_stoppedValue`, `integrable_stoppedValue_of_mem_finset`, `isStoppingTime_const`, `isStoppingTime_of_measurableSet_eq`, `isStoppingTime_piecewise_const`, `measurableSet_preimage_stoppedValue_inter`, `measurable_stoppedValue`, `memLp_stoppedProcess`, `memLp_stoppedProcess_of_mem_finset`, `memLp_stoppedValue`, `memLp_stoppedValue_of_mem_finset`, `progMeasurable_min_stopping_time`, `stoppedProcess_eq`, `stoppedProcess_eq'`, `stoppedProcess_eq''`, `stoppedProcess_eq_of_ge`, `stoppedProcess_eq_of_le`, `stoppedProcess_eq_of_mem_finset`, `stoppedProcess_eq_stoppedValue`, `stoppedProcess_eq_stoppedValue_apply`, `stoppedProcess_indicator_comm`, `stoppedProcess_indicator_comm'`, `stoppedProcess_stoppedProcess`, `stoppedProcess_stoppedProcess'`, `stoppedProcess_stoppedProcess_of_le_left`, `stoppedProcess_stoppedProcess_of_le_right`, `stoppedValue_const`, `stoppedValue_eq`, `stoppedValue_eq'`, `stoppedValue_eq_of_mem_finset`, `stoppedValue_piecewise_const`, `stoppedValue_piecewise_const'`, `stoppedValue_stoppedProcess`, `stoppedValue_stoppedProcess_ae_eq`, `stoppedValue_stoppedProcess_apply`, `stoppedValue_sub_eq_sum`, `stoppedValue_sub_eq_sum'`, `stronglyMeasurable_stoppedValue_of_le`	115
Total	119

MeasureTheory

Definitions

Name	Category	Theorems
`IsStoppingTime` 📖	MathDef	12 math math: `isStoppingTime_piecewise_const`, `StronglyAdapted.isStoppingTime_upperCrossingTime`, `Adapted.isStoppingTime_hittingBtwn`, `StronglyAdapted.isStoppingTime_crossing`, `hittingBtwn_isStoppingTime`, `isStoppingTime_const`, `hittingAfter_isStoppingTime`, `StronglyAdapted.isStoppingTime_lowerCrossingTime`, `StronglyAdapted.isStoppingTime_leastGE`, `isStoppingTime_of_measurableSet_eq`, `hitting_isStoppingTime`, `Adapted.isStoppingTime_hittingAfter`
`stoppedProcess` 📖	CompOp	29 math math: `stoppedProcess_stoppedProcess`, `ProgMeasurable.stronglyAdapted_stoppedProcess`, `stoppedProcess_eq_stoppedValue_apply`, `stoppedProcess_eq_of_ge`, `StronglyAdapted.stoppedProcess`, `integrable_stoppedProcess`, `StronglyAdapted.stoppedProcess_of_discrete`, `stoppedProcess_eq_of_le`, `StronglyAdapted.stronglyMeasurable_stoppedProcess`, `stoppedProcess_indicator_comm'`, `stoppedValue_stoppedProcess_apply`, `stoppedProcess_eq`, `stoppedValue_stoppedProcess`, `Submartingale.stoppedProcess`, `stoppedProcess_stoppedProcess_of_le_left`, `stoppedProcess_eq''`, `memLp_stoppedProcess`, `ProgMeasurable.stronglyMeasurable_stoppedProcess`, `stoppedProcess_eq_of_mem_finset`, `StronglyAdapted.stronglyMeasurable_stoppedProcess_of_discrete`, `stoppedProcess_stoppedProcess_of_le_right`, `stoppedProcess_stoppedProcess'`, `stoppedProcess_eq'`, `integrable_stoppedProcess_of_mem_finset`, `stoppedValue_stoppedProcess_ae_eq`, `ProgMeasurable.stoppedProcess`, `memLp_stoppedProcess_of_mem_finset`, `stoppedProcess_indicator_comm`, `stoppedProcess_eq_stoppedValue`
`stoppedValue` 📖	CompOp	38 math math: `Martingale.stoppedValue_ae_eq_restrict_eq`, `integrable_stoppedValue`, `submartingale_iff_expected_stoppedValue_mono`, `smul_le_stoppedValue_hittingBtwn`, `integrable_stoppedValue_of_mem_finset`, `stoppedValue_hitting_mem`, `stoppedValue_hittingBtwn_mem`, `stoppedProcess_eq_stoppedValue_apply`, `stoppedValue_eq`, `Martingale.stoppedValue_ae_eq_condExp_of_le_of_countable_range`, `stoppedValue_const`, `stoppedValue_lowerCrossingTime`, `Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le`, `stoppedValue_piecewise_const`, `Submartingale.expected_stoppedValue_mono`, `stoppedValue_stoppedProcess_apply`, `Martingale.stoppedValue_min_ae_eq_condExp`, `stoppedValue_upperCrossingTime`, `smul_le_stoppedValue_hitting`, `stoppedValue_stoppedProcess`, `measurableSet_preimage_stoppedValue_inter`, `stoppedValue_sub_eq_sum'`, `memLp_stoppedValue_of_mem_finset`, `Martingale.stoppedValue_ae_eq_condExp_of_le_const`, `le_sub_of_le_upcrossingsBefore`, `stoppedValue_sub_eq_sum`, `memLp_stoppedValue`, `stoppedValue_eq'`, `stoppedValue_stoppedProcess_ae_eq`, `sub_eq_zero_of_upcrossingsBefore_lt`, `Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range`, `stoppedValue_eq_of_mem_finset`, `Submartingale.integrable_stoppedValue`, `measurable_stoppedValue`, `stronglyMeasurable_stoppedValue_of_le`, `Martingale.stoppedValue_ae_eq_condExp_of_le`, `stoppedValue_piecewise_const'`, `stoppedProcess_eq_stoppedValue`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`condExp_min_stopping_time_ae_eq_restrict_le` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `condExp` `IsStoppingTime.measurableSpace` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `IsStoppingTime.min`	—	`IsStoppingTime.min` `IsStoppingTime.measurableSpace_le` `sigmaFiniteTrim_mono` `inf_le_left` `IsStoppingTime.measurableSpace_min` `Filter.EventuallyEq.symm` `Measure.instOuterMeasureClass` `condExp_ae_eq_restrict_of_measurableSpace_eq_on` `IsStoppingTime.measurableSet_le_stopping_time` `Set.inter_comm` `IsStoppingTime.measurableSet_inter_le_iff`
`condExp_min_stopping_time_ae_eq_restrict_le_const` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some` `condExp` `IsStoppingTime.measurableSpace` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `IsStoppingTime.min_const`	—	`IsStoppingTime.min_const` `IsStoppingTime.measurableSpace_le` `sigmaFiniteTrim_mono` `IsStoppingTime.measurableSpace_min_const` `inf_le_left` `Filter.EventuallyEq.symm` `Measure.instOuterMeasureClass` `condExp_ae_eq_restrict_of_measurableSpace_eq_on` `IsStoppingTime.measurableSet_le'` `Set.inter_comm` `IsStoppingTime.measurableSet_inter_le_const_iff`
`condExp_stopping_time_ae_eq_restrict_eq` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `setOf` `WithTop` `WithTop.some` `condExp` `IsStoppingTime.measurableSpace` `Filtration.seq`	—	`IsStoppingTime.measurableSpace_le` `condExp_ae_eq_restrict_of_measurableSpace_eq_on` `Filtration.le` `sigmaFinite_of_sigmaFiniteFiltration` `IsStoppingTime.measurableSet_eq'` `Set.inter_comm` `IsStoppingTime.measurableSet_inter_eq_iff`
`condExp_stopping_time_ae_eq_restrict_eq_of_countable` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `setOf` `WithTop` `WithTop.some` `condExp` `IsStoppingTime.measurableSpace` `Filtration.seq`	—	`IsStoppingTime.measurableSpace_le` `condExp_stopping_time_ae_eq_restrict_eq_of_countable_range` `Set.to_countable` `SetCoe.countable` `WithTop.instCountable`
`condExp_stopping_time_ae_eq_restrict_eq_of_countable_range` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `setOf` `WithTop` `WithTop.some` `condExp` `IsStoppingTime.measurableSpace` `Filtration.seq`	—	`IsStoppingTime.measurableSpace_le` `condExp_ae_eq_restrict_of_measurableSpace_eq_on` `Filtration.le` `sigmaFinite_of_sigmaFiniteFiltration` `IsStoppingTime.measurableSet_eq_of_countable_range'` `Set.inter_comm` `IsStoppingTime.measurableSet_inter_eq_iff`
`integrable_stoppedProcess` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`stoppedProcess`	—	`integrable_stoppedProcess_of_mem_finset` `Finset.coe_Iic` `CanLift.prf` `WithTop.canLift` `LT.lt.le`
`integrable_stoppedProcess_of_mem_finset` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `WithTop` `Set` `Set.instMembership` `Set.image` `WithTop.some` `SetLike.coe` `Finset` `Finset.instSetLike`	`stoppedProcess`	—	`memLp_stoppedProcess_of_mem_finset`
`integrable_stoppedValue` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	`stoppedValue`	—	`integrable_stoppedValue_of_mem_finset` `Finset.coe_Iic` `CanLift.prf` `WithTop.canLift`
`integrable_stoppedValue_of_mem_finset` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `WithTop` `Set` `Set.instMembership` `Set.image` `WithTop.some` `SetLike.coe` `Finset` `Finset.instSetLike`	`stoppedValue`	—	`memLp_stoppedValue_of_mem_finset`
`isStoppingTime_const` 📖	mathematical	—	`IsStoppingTime` `WithTop.some`	—	—
`isStoppingTime_of_measurableSet_eq` 📖	mathematical	`MeasurableSet` `Filtration.seq` `setOf` `WithTop` `WithTop.some`	`IsStoppingTime`	—	`Set.ext` `MeasurableSet.biUnion` `Set.to_countable` `SetCoe.countable` `Filtration.mono`
`isStoppingTime_piecewise_const` 📖	mathematical	`Preorder.toLE` `MeasurableSet` `Filtration.seq`	`IsStoppingTime` `Set.piecewise` `WithTop` `WithTop.some`	—	`IsStoppingTime.piecewise_of_le` `isStoppingTime_const` `le_rfl`
`measurableSet_preimage_stoppedValue_inter` 📖	mathematical	`ProgMeasurable` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStoppingTime` `MeasurableSet`	`Filtration.seq` `Set` `Set.instInter` `Set.preimage` `stoppedValue` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	—	`stronglyMeasurable_stoppedValue_of_le` `IsStoppingTime.min_const` `min_le_right` `Set.ext` `min_eq_left` `MeasurableSet.inter` `StronglyMeasurable.measurable` `IsStoppingTime.measurableSet_le`
`measurable_stoppedValue` 📖	mathematical	`ProgMeasurable` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStoppingTime`	`Measurable` `IsStoppingTime.measurableSpace` `stoppedValue`	—	`stronglyMeasurable_stoppedValue_of_le` `IsStoppingTime.min_const` `min_le_right` `Filter.exists_seq_tendsto` `instIsCountablyGenerated_atTop` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder` `Set.ext` `CanLift.prf` `WithTop.canLift` `Filter.Eventually.exists` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Filter.tendsto_atTop` `MeasurableSet.union` `MeasurableSet.iUnion` `instCountableNat` `Filtration.le` `measurableSet_preimage_stoppedValue_inter` `MeasurableSet.inter` `MeasurableSet.preimage` `Measurable.mono` `StronglyMeasurable.measurable` `ProgMeasurable.stronglyAdapted` `le_rfl` `IsStoppingTime.measurableSet_eq_top`
`memLp_stoppedProcess` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	`stoppedProcess`	—	`memLp_stoppedProcess_of_mem_finset` `Finset.coe_Iic` `CanLift.prf` `WithTop.canLift` `LT.lt.le`
`memLp_stoppedProcess_of_mem_finset` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `WithTop` `Set` `Set.instMembership` `Set.image` `WithTop.some` `SetLike.coe` `Finset` `Finset.instSetLike`	`stoppedProcess`	—	`stoppedProcess_eq_of_mem_finset` `MemLp.add` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MemLp.indicator` `Filtration.le` `IsStoppingTime.measurableSet_ge` `memLp_finset_sum` `IsStoppingTime.measurableSet_eq` `Finset.sum_apply`
`memLp_stoppedValue` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	`stoppedValue`	—	`memLp_stoppedValue_of_mem_finset` `Finset.coe_Iic` `CanLift.prf` `WithTop.canLift`
`memLp_stoppedValue_of_mem_finset` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `WithTop` `Set` `Set.instMembership` `Set.image` `WithTop.some` `SetLike.coe` `Finset` `Finset.instSetLike`	`stoppedValue`	—	`stoppedValue_eq_of_mem_finset` `memLp_finset_sum'` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MemLp.indicator` `Filtration.le` `IsStoppingTime.measurableSet_eq_of_countable_range` `Set.Finite.countable` `Set.Finite.subset` `Set.Finite.image` `Finset.finite_toSet`
`progMeasurable_min_stopping_time` 📖	mathematical	`IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`ProgMeasurable` `WithTop.untopA` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `WithTop.some`	—	`Measurable.stronglyMeasurable` `BorelSpace.opensMeasurable` `Measurable.untopA` `measurable_snd` `Measurable.subtype_val` `Measurable.fst` `measurable_subtype_coe` `measurable_of_restrict_of_restrict_compl` `Measurable.min` `WithTop.instBorelSpace` `TopologicalSpace.instSecondCountableTopologyWithTop` `OrderTopology.to_orderClosedTopology` `TopologicalSpace.instOrderTopologyWithTop` `Measurable.withTop_coe` `measurable_of_Iic` `Set.Iic_top` `Set.ext` `Subtype.prop` `Measurable.comp` `Filtration.mono` `min_le_left` `IsStoppingTime.measurableSet_le` `min_eq_left` `CanLift.prf` `WithTop.canLift` `LE.le.trans` `le_of_lt`
`stoppedProcess_eq` 📖	mathematical	—	`stoppedProcess` `Nat.instLinearOrder` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Set.indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `setOf` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast` `Finset.sum` `Pi.addCommMonoid` `Finset.range`	—	`stoppedProcess_eq''` `Finset.ext` `Finset.mem_Iio` `Finset.mem_range`
`stoppedProcess_eq'` 📖	mathematical	—	`stoppedProcess` `Nat.instLinearOrder` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Set.indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `setOf` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `ENat.instNatCast` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Finset.sum` `Pi.addCommMonoid` `Finset.range`	—	`add_comm` `Pi.add_apply` `Set.indicator_union_of_notMem_inter` `Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Set.mem_setOf` `le_iff_eq_or_lt` `Set.ext` `Set.setOf_or` `stoppedProcess_eq` `Finset.sum_range_succ_comm` `add_assoc`
`stoppedProcess_eq''` 📖	mathematical	—	`stoppedProcess` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Set.indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.some` `Finset.sum` `Pi.addCommMonoid` `Finset.Iio`	—	`Finset.coe_Iio` `CanLift.prf` `WithTop.canLift` `stoppedProcess_eq_of_mem_finset` `Finset.ext` `Finset.Iio_filter_lt` `min_self`
`stoppedProcess_eq_of_ge` 📖	mathematical	`WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.some`	`stoppedProcess` `WithTop.untopA`	—	`WithTop.untopA.congr_simp` `min_eq_right`
`stoppedProcess_eq_of_le` 📖	mathematical	`WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.some`	`stoppedProcess`	—	`WithTop.untopA.congr_simp` `min_eq_left`
`stoppedProcess_eq_of_mem_finset` 📖	mathematical	`WithTop` `Set` `Set.instMembership` `Set.image` `WithTop.some` `SetLike.coe` `Finset` `Finset.instSetLike`	`stoppedProcess` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `Set.indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `setOf` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Finset.sum` `Pi.addCommMonoid` `Finset.filter` `Preorder.toLT` `LinearOrder.toDecidableLT`	—	`Pi.add_apply` `Finset.sum_apply` `le_or_gt` `stoppedProcess_eq_of_le` `Set.indicator_of_mem` `Finset.sum_eq_zero` `Set.indicator_of_notMem` `LT.lt.ne'` `lt_of_lt_of_le` `Finset.mem_filter` `add_zero` `stoppedProcess_eq_of_ge` `le_of_lt` `CanLift.prf` `WithTop.canLift` `WithTop.untopA.congr_simp` `Finset.sum_eq_single_of_mem` `Set.mem_setOf` `not_le` `zero_add`
`stoppedProcess_eq_stoppedValue` 📖	mathematical	—	`stoppedProcess` `stoppedValue` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.some`	—	—
`stoppedProcess_eq_stoppedValue_apply` 📖	mathematical	—	`stoppedProcess` `stoppedValue` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.some`	—	—
`stoppedProcess_indicator_comm` 📖	mathematical	—	`stoppedProcess` `Set.indicator`	—	`Set.indicator_of_mem` `Set.indicator_of_notMem`
`stoppedProcess_indicator_comm'` 📖	mathematical	—	`stoppedProcess` `Set.indicator`	—	`stoppedProcess_indicator_comm`
`stoppedProcess_stoppedProcess` 📖	mathematical	—	`stoppedProcess` `Pi.instMinForall_mathlib` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`WithTop.untopA.congr_simp` `inf_of_le_left` `inf_of_le_right` `min_eq_left` `le_trans` `WithTop.untopA_eq_untop` `WithTop.coe_untop` `WithTop.coe_ne_top` `LT.lt.ne` `lt_of_le_of_lt` `min_le_right` `lt_top_iff_ne_top` `min_assoc` `Pi.inf_apply`
`stoppedProcess_stoppedProcess'` 📖	mathematical	—	`stoppedProcess` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`stoppedProcess_stoppedProcess`
`stoppedProcess_stoppedProcess_of_le_left` 📖	mathematical	`Pi.hasLe` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`stoppedProcess`	—	`stoppedProcess_stoppedProcess` `inf_of_le_right`
`stoppedProcess_stoppedProcess_of_le_right` 📖	mathematical	`Pi.hasLe` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`stoppedProcess`	—	`stoppedProcess_stoppedProcess` `inf_of_le_left`
`stoppedValue_const` 📖	mathematical	—	`stoppedValue` `WithTop.some`	—	—
`stoppedValue_eq` 📖	mathematical	`ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast`	`stoppedValue` `Finset.sum` `Pi.addCommMonoid` `Finset.range` `Set.indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `setOf`	—	`stoppedValue_eq_of_mem_finset` `CanLift.prf` `ENat.canLift` `Set.image_congr` `Finset.coe_range` `WithTop.charZero` `Nat.instCharZero` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`stoppedValue_eq'` 📖	mathematical	`WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	`stoppedValue` `Finset.sum` `Pi.addCommMonoid` `Finset.Iic` `Set.indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `setOf`	—	`stoppedValue_eq_of_mem_finset` `Finset.coe_Iic` `CanLift.prf` `WithTop.canLift`
`stoppedValue_eq_of_mem_finset` 📖	mathematical	`WithTop` `Set` `Set.instMembership` `Set.image` `WithTop.some` `SetLike.coe` `Finset` `Finset.instSetLike`	`stoppedValue` `Finset.sum` `Pi.addCommMonoid` `Set.indicator` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `setOf`	—	`stoppedValue.eq_1` `Finset.sum_apply` `Finset.sum_indicator_eq_sum_filter` `Finset.ext` `WithTop.untopA.congr_simp` `CanLift.prf` `WithTop.canLift` `Finset.sum_singleton`
`stoppedValue_piecewise_const` 📖	mathematical	—	`stoppedValue` `Set.piecewise` `WithTop` `WithTop.some`	—	`stoppedValue.eq_1` `WithTop.untopA.congr_simp` `Set.piecewise_eq_of_mem` `Set.piecewise_eq_of_notMem`
`stoppedValue_piecewise_const'` 📖	mathematical	—	`stoppedValue` `Set.piecewise` `WithTop` `WithTop.some` `Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Compl.compl` `Set` `Set.instCompl`	—	`stoppedValue.eq_1` `WithTop.untopA.congr_simp` `Set.piecewise_eq_of_mem` `Set.indicator_of_mem` `Set.indicator_of_notMem` `add_zero` `Set.piecewise_eq_of_notMem` `zero_add`
`stoppedValue_stoppedProcess` 📖	mathematical	—	`stoppedValue` `stoppedProcess` `WithTop` `Top.top` `WithTop.top` `WithTop.decidableEq` `LinearOrder.toDecidableEq` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop.some` `Classical.arbitrary`	—	`WithTop.untopA.congr_simp` `inf_of_le_left`
`stoppedValue_stoppedProcess_ae_eq` 📖	mathematical	`Filter.Eventually` `WithTop` `Top.top` `WithTop.top` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`Filter.EventuallyEq` `stoppedValue` `stoppedProcess` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Measure.instOuterMeasureClass` `Filter.mp_mem` `Filter.univ_mem'` `stoppedValue_stoppedProcess`
`stoppedValue_stoppedProcess_apply` 📖	mathematical	—	`stoppedValue` `stoppedProcess` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`stoppedValue_stoppedProcess`
`stoppedValue_sub_eq_sum` 📖	mathematical	`Pi.hasLe` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `stoppedValue` `Finset.sum` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Finset.Ico` `Nat.instPreorder` `Nat.instLocallyFiniteOrder` `WithTop.untopA`	—	`WithTop.untopA_mono` `Finset.sum_Ico_eq_sub` `Finset.sum_range_sub` `sub_sub_sub_cancel_right`
`stoppedValue_sub_eq_sum'` 📖	mathematical	`Pi.hasLe` `ENat` `Preorder.toLE` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompletelyDistribLattice.toCompleteLattice` `CompleteLinearOrder.toCompletelyDistribLattice` `instCompleteLinearOrderENat` `ENat.instNatCast`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `stoppedValue` `Finset.sum` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Finset.range` `Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `setOf` `Preorder.toLT`	—	`ne_top_of_le_ne_top` `stoppedValue_sub_eq_sum` `Finset.sum_apply` `Finset.sum_indicator_eq_sum_filter` `Finset.sum_congr` `Finset.ext` `CanLift.prf` `ENat.canLift` `WithTop.untopA.congr_simp` `Nat.instNoMaxOrder` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass`
`stronglyMeasurable_stoppedValue_of_le` 📖	mathematical	`ProgMeasurable` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsStoppingTime` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	`StronglyMeasurable` `Filtration.seq` `stoppedValue`	—	`WithTop.untopA_le` `StronglyMeasurable.comp_measurable` `Measurable.prodMk` `Measurable.untopA` `IsStoppingTime.measurable_of_le` `measurable_id`

MeasureTheory.IsStoppingTime

Definitions

Name	Category	Theorems
`measurableSpace` 📖	CompOp	51 math math: `measurableSet_inter_le_iff`, `MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq`, `measurableSet_eq_of_countable'`, `measurableSet`, `measurableSet_eq_of_countable_range'`, `measurableSet_eq_stopping_time_of_countable`, `measurableSet_ge'`, `MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq`, `measurableSet_le_stopping_time`, `measurableSpace_le_of_countable_range`, `measurableSpace_le_of_le_const`, `measurableSet_inter_le_const_iff`, `MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_of_countable_range`, `measurableSet_eq_stopping_time_min`, `measurableSpace_mono`, `measurableSet_lt_of_countable'`, `MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le`, `measurable`, `measurableSet_eq_stopping_time`, `sigmaFinite_stopping_time`, `sigmaFinite_stopping_time_of_le`, `measurableSpace_le`, `MeasureTheory.Martingale.stoppedValue_min_ae_eq_condExp`, `measurableSpace_min`, `measurableSet_min_iff`, `measurableSet_le'`, `MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable`, `MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq_of_countable_range`, `MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const`, `MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le_const`, `measurableSpace_min_const`, `MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const`, `measurableSpace_le_of_countable`, `measurableSet_lt_of_countable_range'`, `measurableSet_stopping_time_le_min`, `measurableSet_gt'`, `MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const`, `measurableSet_min_const_iff`, `MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range`, `measurableSpace_const`, `measurableSet_ge_of_countable'`, `measurableSet_stopping_time_le`, `le_measurableSpace_of_const_le`, `MeasureTheory.measurable_stoppedValue`, `MeasureTheory.condExp_min_stopping_time_ae_eq_restrict_le`, `measurableSet_lt'`, `measurableSet_ge_of_countable_range'`, `MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le`, `measurableSet_eq'`, `measurableSet_inter_eq_iff`, `measurableSpace_le_of_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Pi.instAdd` `WithTop` `WithTop.add`	—	`Set.ext` `Set.nonempty_Iic_subtype` `WithTop.add_top` `le_of_add_le_right` `MeasurableSet.iUnion` `SetCoe.countable` `MeasurableSet.inter` `measurableSet_eq_le` `TopologicalSpace.SecondCountableTopology.to_firstCountableTopology` `instSecondCountableTopologyOfOrderTopologyOfCountable` `add_const'`
`add_const` 📖	mathematical	`MeasureTheory.IsStoppingTime` `Preorder.toLE` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	`WithTop` `WithTop.add` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `WithTop.some`	—	`Set.ext` `MeasureTheory.Filtration.mono` `sub_le_self`
`add_const'` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`WithTop` `WithTop.add` `WithTop.some`	—	`Set.ext` `MeasurableSet.iUnion` `SetCoe.countable` `measurableSet_eq_le` `TopologicalSpace.SecondCountableTopology.to_firstCountableTopology` `instSecondCountableTopologyOfOrderTopologyOfCountable` `le_of_add_le_left`
`le_measurableSpace_of_const_le` 📖	mathematical	`MeasureTheory.IsStoppingTime` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	`MeasurableSpace` `MeasurableSpace.instLE` `MeasureTheory.Filtration.seq` `measurableSpace`	—	`LE.le.trans` `MeasureTheory.isStoppingTime_const` `Eq.le` `measurableSpace_const` `measurableSpace_mono`
`max` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`WithTop` `SemilatticeSup.toMax` `WithTop.semilatticeSup` `Lattice.toSemilatticeSup`	—	`MeasurableSet.inter`
`max_const` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`WithTop` `SemilatticeSup.toMax` `WithTop.semilatticeSup` `Lattice.toSemilatticeSup` `WithTop.some`	—	`max` `MeasureTheory.isStoppingTime_const`
`measurable` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Measurable` `WithTop` `measurableSpace` `WithTop.instMeasurableSpace`	—	`measurable_of_Iic` `WithTop.instBorelSpace` `TopologicalSpace.instOrderTopologyWithTop` `TopologicalSpace.instSecondCountableTopologyWithTop` `Set.Iic_top` `measurableSet_le'`
`measurable'` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Measurable` `WithTop` `WithTop.instMeasurableSpace`	—	`Measurable.mono` `measurable` `measurableSpace_le` `le_rfl`
`measurableSet` 📖	mathematical	`MeasureTheory.IsStoppingTime`	`MeasurableSet` `measurableSpace` `MeasureTheory.Filtration.seq` `Set` `Set.instInter` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	—	—
`measurableSet_eq` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `WithTop.some`	—	`Set.ext` `MeasurableSet.inter` `measurableSet_le` `measurableSet_ge`
`measurableSet_eq'` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop` `WithTop.some`	—	`Set.univ_inter` `measurableSet_inter_eq_iff` `measurableSet_eq`
`measurableSet_eq_le` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `WithTop.some`	—	`MeasureTheory.Filtration.mono` `measurableSet_eq`
`measurableSet_eq_of_countable` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `WithTop.some`	—	`measurableSet_eq_of_countable_range` `Set.to_countable` `SetCoe.countable` `WithTop.instCountable`
`measurableSet_eq_of_countable'` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop` `WithTop.some`	—	`measurableSet_eq_of_countable_range'` `Set.to_countable` `SetCoe.countable` `WithTop.instCountable`
`measurableSet_eq_of_countable_range` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `WithTop.some`	—	`Set.ext` `Set.iUnion_congr_Prop` `Set.iUnion_exists` `Set.iUnion_iUnion_eq'` `LE.le.eq_or_lt` `le_rfl` `MeasurableSet.diff` `measurableSet_le` `MeasurableSet.biUnion` `Set.iUnion_eq_if` `CanLift.prf` `WithTop.canLift` `ne_top_of_lt` `MeasureTheory.Filtration.mono` `LT.lt.le` `MeasurableSet.empty`
`measurableSet_eq_of_countable_range'` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop` `WithTop.some`	—	`Set.univ_inter` `measurableSet_inter_eq_iff` `measurableSet_eq_of_countable_range`
`measurableSet_eq_stopping_time` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop`	—	`min` `measurableSet_eq_stopping_time_min` `measurableSet_min_iff`
`measurableSet_eq_stopping_time_min` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `min` `setOf`	—	`Set.ext` `min` `MeasurableSet.inter` `measurableSet_stopping_time_le_min` `min_comm`
`measurableSet_eq_stopping_time_of_countable` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop`	—	`measurableSet_eq_stopping_time`
`measurableSet_eq_top` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `setOf` `WithTop` `Top.top` `WithTop.top`	—	`MeasurableSet.preimage` `MeasurableSingletonClass.measurableSet_singleton` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `WithTop.instBorelSpace` `TopologicalSpace.instSecondCountableTopologyWithTop` `T25Space.t2Space` `T3Space.t25Space` `T4Space.t3Space` `T5Space.toT4Space` `OrderTopology.t5Space` `TopologicalSpace.instOrderTopologyWithTop` `measurable'`
`measurableSet_ge` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	—	`Set.ext` `MeasurableSet.compl` `measurableSet_lt`
`measurableSet_ge'` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	—	`Set.ext` `MeasurableSet.union` `measurableSet_eq'` `measurableSet_gt'`
`measurableSet_ge_of_countable` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	—	`measurableSet_ge_of_countable_range` `Set.to_countable` `SetCoe.countable` `WithTop.instCountable`
`measurableSet_ge_of_countable'` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	—	`measurableSet_ge_of_countable_range'` `Set.to_countable` `SetCoe.countable` `WithTop.instCountable`
`measurableSet_ge_of_countable_range` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	—	`Set.ext` `MeasurableSet.compl` `measurableSet_lt_of_countable_range`
`measurableSet_ge_of_countable_range'` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	—	`Set.ext` `MeasurableSet.union` `measurableSet_eq_of_countable_range'` `measurableSet_gt'`
`measurableSet_gt` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `WithTop.some`	—	`Set.ext` `MeasurableSet.compl` `measurableSet_le`
`measurableSet_gt'` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `WithTop.some`	—	`Set.ext` `MeasurableSet.compl` `measurableSet_le'`
`measurableSet_inter_eq_iff` 📖	mathematical	`MeasureTheory.IsStoppingTime`	`MeasurableSet` `measurableSpace` `Set` `Set.instInter` `setOf` `WithTop` `WithTop.some` `MeasureTheory.Filtration.seq`	—	`Set.ext` `Set.inter_assoc` `Set.inter_univ` `MeasureTheory.Filtration.le` `MeasureTheory.Filtration.mono` `Set.inter_empty`
`measurableSet_inter_le` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MeasurableSet` `measurableSpace`	`WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `min` `Set` `Set.instInter` `setOf` `Preorder.toLE` `WithTop.instPreorder`	—	`min` `Set.ext` `MeasurableSet.inter` `measurableSet_le` `BorelSpace.opensMeasurable` `WithTop.instBorelSpace` `OrderTopology.to_orderClosedTopology` `TopologicalSpace.instOrderTopologyWithTop` `TopologicalSpace.instSecondCountableTopologyWithTop` `measurable'` `measurable_of_le` `min_const` `min_le_right`
`measurableSet_inter_le_const_iff` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `Set` `Set.instInter` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `min_const`	—	`min_const` `MeasureTheory.isStoppingTime_const` `min` `measurableSet_min_iff` `measurableSpace_const` `measurableSet` `Set.inter_self` `Set.inter_assoc`
`measurableSet_inter_le_iff` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `Set` `Set.instInter` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `min`	—	`min` `Set.inter_assoc` `Set.inter_self` `measurableSet_inter_le` `measurableSet_min_iff`
`measurableSet_le` 📖	mathematical	`MeasureTheory.IsStoppingTime`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	—	—
`measurableSet_le'` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	—	`MeasureTheory.Filtration.le` `Set.ext` `MeasureTheory.Filtration.mono` `min_le_right`
`measurableSet_le_stopping_time` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder`	—	`measurableSet` `measurableSet_le` `BorelSpace.opensMeasurable` `WithTop.instBorelSpace` `OrderTopology.to_orderClosedTopology` `TopologicalSpace.instOrderTopologyWithTop` `TopologicalSpace.instSecondCountableTopologyWithTop` `measurable'` `Set.ext` `LE.le.trans` `MeasurableSet.inter` `measurable_of_le` `min_const` `min_le_right` `measurableSet_le`
`measurableSet_lt` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `WithTop.some`	—	`exists_lub_Iio` `lub_Iio_eq_self_or_Iio_eq_Iic` `measurableSet_lt_of_isLUB` `WithTop.image_coe_Iio` `WithTop.image_coe_Iic` `MeasureTheory.Filtration.mono` `le_of_isLUB_Iio` `measurableSet_le`
`measurableSet_lt'` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `WithTop.some`	—	`Set.ext` `MeasurableSet.diff` `measurableSet_le'` `measurableSet_eq'`
`measurableSet_lt_le` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `WithTop.some`	—	`MeasureTheory.Filtration.mono` `measurableSet_lt`
`measurableSet_lt_of_countable` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `WithTop.some`	—	`measurableSet_lt_of_countable_range` `Set.to_countable` `SetCoe.countable` `WithTop.instCountable`
`measurableSet_lt_of_countable'` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `WithTop.some`	—	`measurableSet_lt_of_countable_range'` `Set.to_countable` `SetCoe.countable` `WithTop.instCountable`
`measurableSet_lt_of_countable_range` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `WithTop.some`	—	`Set.ext` `MeasurableSet.diff` `measurableSet_le` `measurableSet_eq_of_countable_range`
`measurableSet_lt_of_countable_range'` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `WithTop.some`	—	`Set.ext` `MeasurableSet.diff` `measurableSet_le'` `measurableSet_eq_of_countable_range'`
`measurableSet_lt_of_isLUB` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsLUB` `Preorder.toLE` `Set.Iio`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `WithTop.some`	—	`Set.ext` `isMin_iff_forall_not_lt` `MeasurableSet.empty` `IsLUB.exists_seq_monotone_tendsto` `FirstCountableTopology.nhds_generated_countable` `not_isMin_iff` `mem_nhds_iff` `Set.Ioi_subset_Ici` `le_rfl` `isOpen_Ioi` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `Filter.tendsto_atTop'` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `LE.le.trans_lt` `Set.preimage_iUnion` `MeasurableSet.iUnion` `instCountableNat` `MeasureTheory.Filtration.mono` `LT.lt.le` `measurableSet_le`
`measurableSet_lt_of_pred` 📖	mathematical	`MeasureTheory.IsStoppingTime`	`MeasurableSet` `MeasureTheory.Filtration.seq` `setOf` `WithTop` `Preorder.toLT` `WithTop.instPreorder` `WithTop.some`	—	`Set.ext` `isMin_iff_forall_not_lt` `MeasurableSet.empty` `Order.le_pred_iff_of_not_isMin` `MeasureTheory.Filtration.mono` `Order.pred_le` `measurableSet_le`
`measurableSet_min_const_iff` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `WithTop.some` `min_const` `MeasureTheory.Filtration.seq`	—	`min_const` `measurableSpace_min_const` `MeasurableSpace.measurableSet_inf`
`measurableSet_min_iff` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `min`	—	`min` `measurableSpace_min`
`measurableSet_stopping_time_le` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `setOf` `WithTop` `Preorder.toLE` `WithTop.instPreorder`	—	`min` `measurableSet_stopping_time_le_min` `measurableSet_min_iff`
`measurableSet_stopping_time_le_min` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`MeasurableSet` `measurableSpace` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `min` `setOf` `Preorder.toLE` `WithTop.instPreorder`	—	`min` `Set.univ_inter` `measurableSet_inter_le_iff` `measurableSet_le_stopping_time`
`measurableSpace_const` 📖	mathematical	—	`measurableSpace` `WithTop.some` `MeasureTheory.isStoppingTime_const` `MeasureTheory.Filtration.seq`	—	`MeasurableSpace.ext` `MeasureTheory.isStoppingTime_const` `measurableSet` `Set.inter_univ` `MeasureTheory.Filtration.le` `MeasureTheory.Filtration.mono` `Set.inter_empty` `MeasurableSet.empty`
`measurableSpace_le` 📖	mathematical	`MeasureTheory.IsStoppingTime`	`MeasurableSpace` `MeasurableSpace.instLE` `measurableSpace`	—	—
`measurableSpace_le_of_countable` 📖	mathematical	`MeasureTheory.IsStoppingTime`	`MeasurableSpace` `MeasurableSpace.instLE` `measurableSpace`	—	`measurableSpace_le`
`measurableSpace_le_of_countable_range` 📖	mathematical	`MeasureTheory.IsStoppingTime`	`MeasurableSpace` `MeasurableSpace.instLE` `measurableSpace`	—	`measurableSpace_le`
`measurableSpace_le_of_le` 📖	mathematical	`MeasureTheory.IsStoppingTime` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	`MeasurableSpace` `MeasurableSpace.instLE` `measurableSpace`	—	`LE.le.trans` `measurableSpace_le_of_le_const` `MeasureTheory.Filtration.le`
`measurableSpace_le_of_le_const` 📖	mathematical	`MeasureTheory.IsStoppingTime` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	`MeasurableSpace` `MeasurableSpace.instLE` `measurableSpace` `MeasureTheory.Filtration.seq`	—	`LE.le.trans` `MeasureTheory.isStoppingTime_const` `measurableSpace_mono` `Eq.le` `measurableSpace_const`
`measurableSpace_min` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`measurableSpace` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `min` `MeasurableSpace` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice`	—	`le_antisymm` `min` `le_inf` `measurableSpace_mono` `min_le_left` `min_le_right` `Set.ext` `Set.inter_union_distrib_left` `MeasurableSet.union`
`measurableSpace_min_const` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`measurableSpace` `WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `WithTop.some` `min_const` `MeasurableSpace` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `MeasurableSpace.instCompleteLattice` `MeasureTheory.Filtration.seq`	—	`min_const` `MeasureTheory.isStoppingTime_const` `min` `measurableSpace_min` `measurableSpace_const`
`measurableSpace_mono` 📖	mathematical	`MeasureTheory.IsStoppingTime` `Pi.hasLe` `WithTop` `Preorder.toLE` `WithTop.instPreorder`	`MeasurableSpace` `MeasurableSpace.instLE` `measurableSpace`	—	`Set.ext` `le_trans` `MeasurableSet.inter`
`measurable_of_le` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	`Measurable` `MeasureTheory.Filtration.seq` `WithTop.instMeasurableSpace`	—	`Measurable.mono` `measurable` `measurableSpace_le_of_le_const` `le_rfl`
`min` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf`	—	`MeasurableSet.union`
`min_const` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`WithTop` `SemilatticeInf.toMin` `WithTop.semilatticeInf` `WithTop.some`	—	`min` `MeasureTheory.isStoppingTime_const`
`piecewise_of_le` 📖	mathematical	`MeasureTheory.IsStoppingTime` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some` `MeasurableSet` `MeasureTheory.Filtration.seq`	`Set.piecewise`	—	`Set.ext` `MeasureTheory.Filtration.mono` `MeasurableSet.union` `MeasurableSet.inter` `MeasurableSet.compl` `LE.le.trans` `Set.inter_empty` `Set.union_self` `MeasurableSet.empty`
`sigmaFinite_stopping_time` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	`MeasureTheory.SigmaFinite` `measurableSpace` `MeasureTheory.Measure.trim` `measurableSpace_le`	—	`MeasureTheory.sigmaFiniteTrim_mono` `measurableSpace_le` `le_measurableSpace_of_const_le` `bot_le` `LE.le.trans` `MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration`
`sigmaFinite_stopping_time_of_le` 📖	mathematical	`MeasureTheory.IsStoppingTime` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `WithTop` `Preorder.toLE` `WithTop.instPreorder` `WithTop.some`	`MeasureTheory.SigmaFinite` `measurableSpace` `MeasureTheory.Measure.trim` `measurableSpace_le_of_le`	—	`MeasureTheory.sigmaFiniteTrim_mono` `measurableSpace_le_of_le` `le_measurableSpace_of_const_le` `bot_le` `LE.le.trans` `MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration`

MeasureTheory.ProgMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stoppedProcess` 📖	mathematical	`MeasureTheory.ProgMeasurable` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MeasureTheory.IsStoppingTime`	`MeasureTheory.stoppedProcess`	—	`MeasureTheory.progMeasurable_min_stopping_time` `comp` `WithTop.untopA.congr_simp` `inf_of_le_left` `le_total` `inf_of_le_right`
`stronglyAdapted_stoppedProcess` 📖	mathematical	`MeasureTheory.ProgMeasurable` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MeasureTheory.IsStoppingTime`	`MeasureTheory.StronglyAdapted` `MeasureTheory.stoppedProcess`	—	`stronglyAdapted` `stoppedProcess`
`stronglyMeasurable_stoppedProcess` 📖	mathematical	`MeasureTheory.ProgMeasurable` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MeasureTheory.IsStoppingTime`	`MeasureTheory.StronglyMeasurable` `MeasureTheory.stoppedProcess`	—	`MeasureTheory.StronglyMeasurable.mono` `stronglyAdapted_stoppedProcess` `MeasureTheory.Filtration.le`

MeasureTheory.StronglyAdapted

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`stoppedProcess` 📖	mathematical	`MeasureTheory.StronglyAdapted` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Continuous` `MeasureTheory.IsStoppingTime`	`MeasureTheory.stoppedProcess`	—	`MeasureTheory.ProgMeasurable.stronglyAdapted` `MeasureTheory.ProgMeasurable.stoppedProcess` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `progMeasurable_of_continuous` `BorelSpace.opensMeasurable`
`stoppedProcess_of_discrete` 📖	mathematical	`MeasureTheory.StronglyAdapted` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MeasureTheory.IsStoppingTime`	`MeasureTheory.stoppedProcess`	—	`MeasureTheory.ProgMeasurable.stronglyAdapted` `MeasureTheory.ProgMeasurable.stoppedProcess` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `TopologicalSpace.DiscreteTopology.metrizableSpace` `progMeasurable_of_discrete` `BorelSpace.opensMeasurable`
`stronglyMeasurable_stoppedProcess` 📖	mathematical	`MeasureTheory.StronglyAdapted` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Continuous` `MeasureTheory.IsStoppingTime`	`MeasureTheory.StronglyMeasurable` `MeasureTheory.stoppedProcess`	—	`MeasureTheory.ProgMeasurable.stronglyMeasurable_stoppedProcess` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `progMeasurable_of_continuous` `BorelSpace.opensMeasurable`
`stronglyMeasurable_stoppedProcess_of_discrete` 📖	mathematical	`MeasureTheory.StronglyAdapted` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MeasureTheory.IsStoppingTime`	`MeasureTheory.StronglyMeasurable` `MeasureTheory.stoppedProcess`	—	`MeasureTheory.ProgMeasurable.stronglyMeasurable_stoppedProcess` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `TopologicalSpace.DiscreteTopology.metrizableSpace` `progMeasurable_of_discrete` `BorelSpace.opensMeasurable`

---

← Back to Index