Stopping

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

Statistics

Metric	Count
Definitions IsStoppingTime, measurableSpace, stoppedProcess, stoppedValue	4
Theorems add, add_const, add_const', biInf, iInf, 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_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_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_of_measurableSet_lt_of_isRightContinuous, isStoppingTime_of_measurableSet_lt_of_isRightContinuous', 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	116
Total	120

MeasureTheory

Definitions

Name	Category	Theorems
IsStoppingTime 📖	MathDef	27 math math: IsStoppingTime.add, isStoppingTime_piecewise_const, IsStoppingTime.iInf, StronglyAdapted.isStoppingTime_upperCrossingTime, IsStoppingTime.add_const', IsStoppingTime.min, isStoppingTime_of_measurableSet_lt_of_isRightContinuous, Adapted.isStoppingTime_hittingBtwn, isStoppingTime_of_measurableSet_lt_of_isRightContinuous', isStoppingTime_hittingBtwn_isStoppingTime, StronglyAdapted.isStoppingTime_crossing, hittingBtwn_isStoppingTime, IsStoppingTime.min_const, isStoppingTime_const, hittingAfter_isStoppingTime, isStoppingTime_hitting_isStoppingTime, StronglyAdapted.isStoppingTime_lowerCrossingTime, IsStoppingTime.max, StronglyAdapted.isStoppingTime_leastGE, IsStoppingTime.add_const, IsStoppingTime.biInf, isStoppingTime_of_measurableSet_eq, IsStoppingTime.piecewise_of_le, Adapted.isStoppingTime_hittingBtwn_isStoppingTime, IsStoppingTime.max_const, 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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	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	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup 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	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup 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	Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup 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_of_measurableSet_lt_of_isRightContinuous 📖	mathematical	MeasurableSet Filtration.seq PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice setOf WithTop Preorder.toLT WithTop.instPreorder WithTop.some	IsStoppingTime PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	—	isStoppingTime_of_measurableSet_lt_of_isRightContinuous' Filter.NeBot.ne nhdsGT_neBot
isStoppingTime_of_measurableSet_lt_of_isRightContinuous' 📖	mathematical	MeasurableSet Filtration.seq PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice setOf WithTop Preorder.toLT WithTop.instPreorder WithTop.some	IsStoppingTime PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	—	Set.ext MeasurableSet.union Filter.Eventually.frequently eventually_nhdsWithin_of_forall Filter.exists_seq_forall_of_frequently TopologicalSpace.isCountablyGenerated_nhdsWithin FirstCountableTopology.nhds_generated_countable Filter.Eventually.exists Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.eventually_lt_const instClosedIciTopology OrderTopology.to_orderClosedTopology Filter.Tendsto.comp ContinuousAt.tendsto Continuous.continuousAt WithTop.continuous_coe TopologicalSpace.instOrderTopologyWithTop LE.le.trans_lt le_of_forall_gt LT.lt.trans Filtration.IsRightContinuous.eq Filtration.rightCont_eq_of_neBot_nhdsGT le_antisymm iInf_congr_Prop iInf₂_le LE.le.trans iInf_le Filtration.mono LT.lt.le le_total LT.lt.trans_le le_rfl MeasurableSet.iInter instCountableNat Prop.countable
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	MeasurableSet Filtration.seq PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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	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	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace 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	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace 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	MemLp ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toPseudoMetricSpace 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 instLEENat 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 instLEENat instAddENat ENat.instNatCast AddMonoidWithOne.toOne instAddMonoidWithOneENat Finset.sum Pi.addCommMonoid Finset.range	—	add_comm Pi.add_apply Set.indicator_union_of_notMem_inter Nat.cast_one IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid 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 WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop.some 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 instLEENat ENat.instNatCast	stoppedValue Finset.sum Pi.addCommMonoid Finset.range Set.indicator AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid setOf ENat ENat.instNatCast	—	stoppedValue_eq_of_mem_finset CanLift.prf ENat.canLift Set.image_congr Finset.coe_range WithTop.charZero Nat.instCharZero IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
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 WithTop WithTop.some	—	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 WithTop WithTop.some	—	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 ae Measure Measure.instFunLike Measure.instOuterMeasureClass stoppedValue stoppedProcess WithTop 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 instLEENat	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 instLEENat 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 ENat instLEENat ENat.instNatCast instLTENat	—	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
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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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	49 math math: measurableSet_inter_le_iff, MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq, measurableSet_eq_of_countable', measurableSet, measurableSet_eq_of_countable_range', measurableSet_ge', MeasureTheory.condExp_stopping_time_ae_eq_restrict_eq, measurableSet_le_stopping_time, 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, measurableSet_inter_le, 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	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	MeasureTheory.IsStoppingTime 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	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
biInf 📖	mathematical	MeasureTheory.IsStoppingTime PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder	MeasureTheory.IsStoppingTime PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder iInf WithTop WithTop.instInfSet ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set Set.instMembership	—	MeasureTheory.isStoppingTime_of_measurableSet_lt_of_isRightContinuous MeasurableSet.of_compl Set.ext MeasurableSet.biInter measurableSet_ge
iInf 📖	mathematical	MeasureTheory.IsStoppingTime PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder	MeasureTheory.IsStoppingTime PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder iInf WithTop WithTop.instInfSet ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	iInf_congr_Prop iInf_pos biInf Set.countable_univ
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	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	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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder setOf WithTop WithTop.some	—	MeasureTheory.Filtration.mono measurableSet_eq
measurableSet_eq_of_countable 📖	mathematical	MeasureTheory.IsStoppingTime PartialOrder.toPreorder	MeasurableSet MeasureTheory.Filtration.seq PartialOrder.toPreorder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder WithTop SemilatticeInf.toMin WithTop.semilatticeInf min setOf	—	Set.ext min MeasurableSet.inter measurableSet_stopping_time_le_min min_comm
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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 instReflLe 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	MeasurableSet measurableSpace PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder setOf WithTop Preorder.toLE WithTop.instPreorder	—	measurableSet measurableSet_le BorelSpace.opensMeasurable WithTop.instBorelSpace OrderTopology.to_orderClosedTopology TopologicalSpace.instOrderTopologyWithTop TopologicalSpace.instSecondCountableTopologyWithTop measurable' Set.ext instIsPreorder_mathlib 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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_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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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 WithTop MeasureTheory.Filtration.seq PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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	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	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	MeasureTheory.IsStoppingTime Set.piecewise WithTop	—	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 PartialOrder.toPreorder SemilatticeSup.toPartialOrder 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 PartialOrder.toPreorder SemilatticeSup.toPartialOrder 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.ProgMeasurable PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MeasureTheory.stoppedProcess	—	MeasureTheory.progMeasurable_min_stopping_time comp WithTop.untopA.congr_simp inf_of_le_left instReflLe le_total inf_of_le_right
stronglyAdapted_stoppedProcess 📖	mathematical	MeasureTheory.ProgMeasurable PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MeasureTheory.IsStoppingTime	MeasureTheory.StronglyAdapted PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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.StronglyAdapted PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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.StronglyAdapted PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder 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