HittingTime

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

Statistics

Metric	Count
Definitions hitting, hittingAfter, hittingBtwn	3
Theorems isStoppingTime_hittingAfter, isStoppingTime_hittingBtwn, isStoppingTime_hittingBtwn_isStoppingTime, hittingAfter_anti, hittingAfter_apply_anti, hittingAfter_apply_mono, hittingAfter_bot_le_iff, hittingAfter_def, hittingAfter_empty, hittingAfter_eq_sInf, hittingAfter_eq_top_iff, hittingAfter_isStoppingTime, hittingAfter_le_iff, hittingAfter_le_of_mem, hittingAfter_lt_iff, hittingAfter_mem_set, hittingAfter_mem_set_of_ne_top, hittingAfter_mono, hittingAfter_univ, hittingBtwn_anti, hittingBtwn_apply_anti, hittingBtwn_apply_mono_left, hittingBtwn_apply_mono_right, hittingBtwn_bot_le_iff, hittingBtwn_def, hittingBtwn_empty, hittingBtwn_eq_end_iff, hittingBtwn_eq_hittingBtwn_of_exists, hittingBtwn_eq_sInf, hittingBtwn_isStoppingTime, hittingBtwn_le, hittingBtwn_le_iff_of_exists, hittingBtwn_le_iff_of_lt, hittingBtwn_le_of_mem, hittingBtwn_lt_iff, hittingBtwn_mem_Icc, hittingBtwn_mem_set, hittingBtwn_mem_set_of_hittingBtwn_lt, hittingBtwn_mono, hittingBtwn_mono_left, hittingBtwn_mono_right, hittingBtwn_of_le, hittingBtwn_of_lt, hittingBtwn_univ, hitting_bot_le_iff, hitting_def, hitting_eq_end_iff, hitting_eq_hitting_of_exists, hitting_eq_sInf, hitting_isStoppingTime, hitting_le, hitting_le_iff_of_exists, hitting_le_iff_of_lt, hitting_le_of_mem, hitting_lt_iff, hitting_mem_Icc, hitting_mem_set, hitting_mem_set_of_hitting_lt, hitting_mono, hitting_of_le, hitting_of_lt, isStoppingTime_hittingBtwn_isStoppingTime, isStoppingTime_hitting_isStoppingTime, le_hitting, le_hittingAfter, le_hittingBtwn, le_hittingBtwn_of_exists, le_hitting_of_exists, notMem_of_lt_hitting, notMem_of_lt_hittingAfter, notMem_of_lt_hittingBtwn, stoppedValue_hittingBtwn_mem, stoppedValue_hitting_mem	73
Total	76

MeasureTheory

Definitions

Name	Category	Theorems
hitting 📖	CompOp	—
hittingAfter 📖	CompOp	18 math math: hittingAfter_bot_le_iff, hittingAfter_mono, hittingAfter_mem_set, hittingAfter_def, hittingAfter_eq_top_iff, hittingAfter_univ, hittingAfter_apply_anti, hittingAfter_eq_sInf, hittingAfter_mem_set_of_ne_top, hittingAfter_isStoppingTime, hittingAfter_empty, hittingAfter_le_iff, hittingAfter_apply_mono, le_hittingAfter, hittingAfter_le_of_mem, hittingAfter_anti, hittingAfter_lt_iff, Adapted.isStoppingTime_hittingAfter
hittingBtwn 📖	CompOp	55 math math: hittingBtwn_apply_mono_right, hittingBtwn_mono_left, upperCrossingTime_succ_eq, le_hitting_of_exists, smul_le_stoppedValue_hittingBtwn, hittingBtwn_univ, le_hitting, hittingBtwn_mem_Icc, hitting_le_of_mem, hittingBtwn_mem_set, stoppedValue_hitting_mem, hittingBtwn_mono, stoppedValue_hittingBtwn_mem, hitting_le_iff_of_exists, hittingBtwn_apply_anti, hittingBtwn_bot_le_iff, Adapted.isStoppingTime_hittingBtwn, hitting_mem_Icc, lowerCrossingTime_zero, le_hittingBtwn, hitting_eq_end_iff, hittingBtwn_le_of_mem, isStoppingTime_hittingBtwn_isStoppingTime, hitting_le, hittingBtwn_apply_mono_left, hittingBtwn_anti, hitting_def, smul_le_stoppedValue_hitting, hitting_bot_le_iff, hittingBtwn_mono_right, hittingBtwn_empty, hittingBtwn_isStoppingTime, hitting_eq_hitting_of_exists, hitting_mono, hitting_lt_iff, hittingBtwn_le, hittingBtwn_eq_sInf, hittingBtwn_le_iff_of_lt, hittingBtwn_eq_end_iff, hitting_mem_set, isStoppingTime_hitting_isStoppingTime, upperCrossingTime_succ, hittingBtwn_of_lt, hittingBtwn_lt_iff, hitting_of_le, hitting_of_lt, hittingBtwn_of_le, hitting_eq_sInf, hittingBtwn_le_iff_of_exists, hitting_le_iff_of_lt, hittingBtwn_def, Adapted.isStoppingTime_hittingBtwn_isStoppingTime, le_hittingBtwn_of_exists, hitting_isStoppingTime, hittingBtwn_eq_hittingBtwn_of_exists

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hittingAfter_anti 📖	mathematical	—	Antitone Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Pi.preorder WithTop WithTop.instPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingAfter ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csInf_le_csInf Set.setOf_subset_setOf_of_imp Mathlib.Tactic.GCongr.and_right_mono Set.mem_of_subset_of_mem
hittingAfter_apply_anti 📖	mathematical	—	Antitone Set WithTop PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra WithTop.instPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingAfter ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingAfter_anti
hittingAfter_apply_mono 📖	mathematical	—	Monotone WithTop PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice WithTop.instPreorder hittingAfter ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingAfter_mono
hittingAfter_bot_le_iff 📖	mathematical	—	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder hittingAfter ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Bot.bot OrderBot.toBot SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrderBot.toOrderBot WithTop.some Set Set.instMembership	—	Set.Icc_bot
hittingAfter_def 📖	mathematical	—	hittingAfter WithTop Preorder.toLE Set Set.instMembership WithTop.some InfSet.sInf setOf Top.top WithTop.top	—	—
hittingAfter_empty 📖	mathematical	—	hittingAfter Set Set.instEmptyCollection Top.top WithTop WithTop.top	—	infSet_to_nonempty
hittingAfter_eq_sInf 📖	mathematical	—	hittingAfter PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Bot.bot OrderBot.toBot Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder WithTop Set Set.instMembership WithTop.some InfSet.sInf setOf Top.top WithTop.top	—	—
hittingAfter_eq_top_iff 📖	mathematical	—	hittingAfter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Top.top WithTop WithTop.top Set Set.instMembership	—	—
hittingAfter_isStoppingTime 📖	mathematical	Adapted PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice MeasurableSet	IsStoppingTime hittingAfter ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	Adapted.isStoppingTime_hittingAfter
hittingAfter_le_iff 📖	mathematical	—	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingAfter ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf WithTop.some Set Set.instMembership Set.Icc	—	le_hittingAfter supSet_to_nonempty CanLift.prf WithTop.canLift WithTop.untopA.congr_simp hittingAfter_mem_set_of_ne_top le_trans hittingAfter_le_of_mem
hittingAfter_le_of_mem 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set Set.instMembership	WithTop WithTop.instPreorder hittingAfter ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf WithTop.some	—	hittingAfter.eq_1 csInf_le BddBelow.inter_of_left bddBelow_Ici Set.mem_inter
hittingAfter_lt_iff 📖	mathematical	—	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingAfter ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf WithTop.some Set Set.instMembership Set.Ico	—	le_hittingAfter supSet_to_nonempty CanLift.prf WithTop.canLift WithTop.untopA.congr_simp hittingAfter_mem_set_of_ne_top lt_of_le_of_lt hittingAfter_le_of_mem
hittingAfter_mem_set 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set Set.instMembership	WithTop.untopA supSet_to_nonempty ConditionallyCompletePartialOrderSup.toSupSet hittingAfter ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	supSet_to_nonempty hittingAfter.eq_1 Set.mem_inter csInf_mem
hittingAfter_mem_set_of_ne_top 📖	mathematical	—	Set Set.instMembership WithTop.untopA supSet_to_nonempty ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingAfter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	supSet_to_nonempty hittingAfter_mem_set
hittingAfter_mono 📖	mathematical	—	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Pi.preorder WithTop WithTop.instPreorder hittingAfter ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csInf_le_csInf Set.setOf_subset_setOf_of_imp le_imp_le_of_le_of_le le_refl LE.le.trans
hittingAfter_univ 📖	mathematical	—	hittingAfter PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.univ WithTop.some	—	le_rfl csInf_Ici
hittingBtwn_anti 📖	mathematical	—	Antitone Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Pi.preorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csInf_le_csInf Set.inter_subset_inter subset_refl Set.instReflSubset Set.setOf_subset_setOf_of_imp Set.mem_of_subset_of_mem csInf_le_of_le
hittingBtwn_apply_anti 📖	mathematical	—	Antitone Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingBtwn_anti
hittingBtwn_apply_mono_left 📖	mathematical	—	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingBtwn_mono_left
hittingBtwn_apply_mono_right 📖	mathematical	—	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingBtwn_mono_right
hittingBtwn_bot_le_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Set Set.instMembership	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Bot.bot OrderBot.toBot SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrderBot.toOrderBot	—	lt_or_ge hittingBtwn_le_iff_of_lt Set.Icc_bot LE.le.trans hittingBtwn_le
hittingBtwn_def 📖	mathematical	—	hittingBtwn Set Set.instMembership Set.Icc InfSet.sInf Set.instInter setOf	—	—
hittingBtwn_empty 📖	mathematical	—	hittingBtwn Set Set.instEmptyCollection	—	infSet_to_nonempty
hittingBtwn_eq_end_iff 📖	mathematical	—	hittingBtwn PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf InfSet.sInf Set Set.instInter Set.Icc setOf Set.instMembership	—	hittingBtwn.eq_1
hittingBtwn_eq_hittingBtwn_of_exists 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set Set.instMembership Set.Icc	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	LE.le.trans le_antisymm le_csInf Set.Icc_subset_Icc_right csInf_le BddBelow.inter_of_left bddBelow_Icc le_of_not_ge csInf_le_csInf Set.inter_subset_inter Set.Icc_subset_Icc le_refl subset_refl Set.instReflSubset
hittingBtwn_eq_sInf 📖	mathematical	—	hittingBtwn PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Bot.bot OrderBot.toBot Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Top.top OrderTop.toTop BoundedOrder.toOrderTop InfSet.sInf setOf Set Set.instMembership	—	Set.Icc_bot Set.Iic_top Set.univ_inter sInf_eq_top
hittingBtwn_isStoppingTime 📖	mathematical	Adapted PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice MeasurableSet	IsStoppingTime WithTop.some hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	Adapted.isStoppingTime_hittingBtwn
hittingBtwn_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	LE.le.trans csInf_le BddBelow.inter_of_left bddBelow_Icc Set.mem_inter le_rfl
hittingBtwn_le_iff_of_exists 📖	mathematical	Set Set.instMembership Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Preorder.toLE hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	le_hittingBtwn_of_exists hittingBtwn_mem_set le_min min_le_min min_rec' le_trans hittingBtwn_le_of_mem LE.le.trans min_le_left min_le_right
hittingBtwn_le_iff_of_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Preorder.toLE hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set Set.instMembership Set.Icc	—	hittingBtwn_le_iff_of_exists not_le Mathlib.Tactic.Push.not_and_eq LE.le.trans LT.lt.le
hittingBtwn_le_of_mem 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set Set.instMembership	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csInf_le BddBelow.inter_of_left bddBelow_Icc Set.mem_inter
hittingBtwn_lt_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Preorder.toLT hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set Set.instMembership Set.Ico	—	le_hittingBtwn_of_exists hittingBtwn_mem_set lt_of_le_of_lt hittingBtwn_le_of_mem LE.le.trans LT.lt.le
hittingBtwn_mem_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Set Set.instMembership Set.Icc hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	le_hittingBtwn hittingBtwn_le
hittingBtwn_mem_set 📖	mathematical	Set Set.instMembership Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	Set.mem_inter csInf_mem Set.mem_inter_iff
hittingBtwn_mem_set_of_hittingBtwn_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	Set Set.instMembership	—	hittingBtwn_mem_set LT.lt.ne
hittingBtwn_mono 📖	mathematical	—	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingBtwn_mono_right
hittingBtwn_mono_left 📖	mathematical	—	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Pi.preorder hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	csInf_le_csInf Set.inter_subset_inter Set.Icc_subset_Icc le_refl subset_refl Set.instReflSubset csInf_le_of_le LE.le.trans
hittingBtwn_mono_right 📖	mathematical	—	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	Eq.le hittingBtwn_eq_hittingBtwn_of_exists le_csInf Mathlib.Tactic.Push.not_forall_eq LT.lt.le
hittingBtwn_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	le_iff_eq_or_lt hittingBtwn.eq_1 Set.mem_Icc Set.Icc_self Set.inter_eq_left Set.singleton_subset_iff le_antisymm csInf_singleton hittingBtwn_of_lt
hittingBtwn_of_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	—
hittingBtwn_univ 📖	mathematical	—	hittingBtwn PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.univ SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice	—	Set.inter_univ csInf_Icc inf_of_le_left Set.Icc_eq_empty
hitting_bot_le_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder Set Set.instMembership	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Bot.bot OrderBot.toBot SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrderBot.toOrderBot	—	hittingBtwn_bot_le_iff
hitting_def 📖	mathematical	—	hittingBtwn Set Set.instMembership Set.Icc InfSet.sInf Set.instInter setOf	—	hittingBtwn_def
hitting_eq_end_iff 📖	mathematical	—	hittingBtwn PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf InfSet.sInf Set Set.instInter Set.Icc setOf Set.instMembership	—	hittingBtwn_eq_end_iff
hitting_eq_hitting_of_exists 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set Set.instMembership Set.Icc	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingBtwn_eq_hittingBtwn_of_exists
hitting_eq_sInf 📖	mathematical	—	hittingBtwn PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Bot.bot OrderBot.toBot Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Top.top OrderTop.toTop BoundedOrder.toOrderTop InfSet.sInf setOf Set Set.instMembership	—	hittingBtwn_eq_sInf
hitting_isStoppingTime 📖	mathematical	Adapted PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice MeasurableSet	IsStoppingTime WithTop.some hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	Adapted.isStoppingTime_hittingBtwn
hitting_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingBtwn_le
hitting_le_iff_of_exists 📖	mathematical	Set Set.instMembership Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Preorder.toLE hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingBtwn_le_iff_of_exists
hitting_le_iff_of_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Preorder.toLE hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set Set.instMembership Set.Icc	—	hittingBtwn_le_iff_of_lt
hitting_le_of_mem 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Set Set.instMembership	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingBtwn_le_of_mem
hitting_lt_iff 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Preorder.toLT hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set Set.instMembership Set.Ico	—	hittingBtwn_lt_iff
hitting_mem_Icc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Set Set.instMembership Set.Icc hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingBtwn_mem_Icc
hitting_mem_set 📖	mathematical	Set Set.instMembership Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingBtwn_mem_set
hitting_mem_set_of_hitting_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	Set Set.instMembership	—	hittingBtwn_mem_set_of_hittingBtwn_lt
hitting_mono 📖	mathematical	—	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingBtwn_mono_right
hitting_of_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingBtwn_of_le
hitting_of_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	hittingBtwn_of_lt
isStoppingTime_hittingBtwn_isStoppingTime 📖	mathematical	IsStoppingTime PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice WithTop Preorder.toLE WithTop.instPreorder WithTop.some MeasurableSet Adapted	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf WithTop.untopA supSet_to_nonempty ConditionallyCompletePartialOrderSup.toSupSet	—	Adapted.isStoppingTime_hittingBtwn_isStoppingTime
isStoppingTime_hitting_isStoppingTime 📖	mathematical	IsStoppingTime PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice WithTop Preorder.toLE WithTop.instPreorder WithTop.some MeasurableSet Adapted	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf WithTop.untopA supSet_to_nonempty ConditionallyCompletePartialOrderSup.toSupSet	—	Adapted.isStoppingTime_hittingBtwn_isStoppingTime
le_hitting 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	le_hittingBtwn
le_hittingAfter 📖	mathematical	—	WithTop Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice WithTop.some hittingAfter ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	le_csInf
le_hittingBtwn 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	le_csInf Set.mem_inter_iff
le_hittingBtwn_of_exists 📖	mathematical	Set Set.instMembership Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Preorder.toLE hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	le_hittingBtwn supSet_to_nonempty Set.Icc_eq_empty_of_lt not_le
le_hitting_of_exists 📖	mathematical	Set Set.instMembership Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Preorder.toLE hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	le_hittingBtwn_of_exists
notMem_of_lt_hitting 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Preorder.toLE	Set Set.instMembership	—	notMem_of_lt_hittingBtwn
notMem_of_lt_hittingAfter 📖	mathematical	WithTop Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice WithTop.some hittingAfter ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Preorder.toLE	Set Set.instMembership	—	not_le hittingAfter.eq_1 csInf_le BddBelow.inter_of_left bddBelow_Ici
notMem_of_lt_hittingBtwn 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Preorder.toLE	Set Set.instMembership	—	le_trans LT.lt.le hittingBtwn_le not_le csInf_le BddBelow.inter_of_left bddBelow_Icc
stoppedValue_hittingBtwn_mem 📖	mathematical	Set Set.instMembership Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	stoppedValue supSet_to_nonempty ConditionallyCompletePartialOrderSup.toSupSet WithTop.some hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	supSet_to_nonempty WithTop.untopA.congr_simp csInf_mem Set.nonempty_of_mem
stoppedValue_hitting_mem 📖	mathematical	Set Set.instMembership Set.Icc PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	stoppedValue supSet_to_nonempty ConditionallyCompletePartialOrderSup.toSupSet WithTop.some hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	stoppedValue_hittingBtwn_mem

MeasureTheory.Adapted

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStoppingTime_hittingAfter 📖	mathematical	MeasureTheory.Adapted PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice MeasurableSet	MeasureTheory.IsStoppingTime MeasureTheory.hittingAfter ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	Set.ext Set.iUnion_congr_Prop MeasurableSet.iUnion Prop.countable MeasureTheory.Filtration.mono
isStoppingTime_hittingBtwn 📖	mathematical	MeasureTheory.Adapted PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice MeasurableSet	MeasureTheory.IsStoppingTime WithTop.some MeasureTheory.hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	le_or_gt LE.le.trans MeasureTheory.hittingBtwn_le Set.ext MeasureTheory.hittingBtwn_le_iff_of_lt Set.iUnion_congr_Prop MeasurableSet.iUnion Prop.countable MeasureTheory.Filtration.mono
isStoppingTime_hittingBtwn_isStoppingTime 📖	mathematical	MeasureTheory.IsStoppingTime PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice WithTop Preorder.toLE WithTop.instPreorder WithTop.some MeasurableSet MeasureTheory.Adapted	MeasureTheory.hittingBtwn ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf WithTop.untopA supSet_to_nonempty ConditionallyCompletePartialOrderSup.toSupSet	—	supSet_to_nonempty Set.ext Set.iUnion_congr_Prop CanLift.prf WithTop.canLift WithTop.untopA.congr_simp LT.lt.trans_le MeasureTheory.le_hittingBtwn Set.union_empty MeasurableSet.iUnion Prop.countable MeasurableSet.inter MeasureTheory.Filtration.mono MeasureTheory.IsStoppingTime.measurableSet_eq isStoppingTime_hittingBtwn

---

← Back to Index