Theorems · Theorem · probability

MeasureTheory.hittingBtwn_mono_right

∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {ω : Ω} (u : ι → Ω → β)
  (s : Set β) (n : ι), Monotone fun x => MeasureTheory.hittingBtwn u s n x ω

hittingBtwn is monotone with respect to the maximal time.

Defined in

Mathlib.Probability.Process.HittingTime

Cited by

1 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

ConditionallyCompleteLinearOrder