Strict infimum crossings and passage times

Reference: J. Bertoin, Lévy Processes, Cambridge University Press, 1996, Chapters IV and VI.

theorem BGW.StableTrees.ae_localTime_gt_iff_passageTime_lt {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (x t : NNReal), ↑x < localTime f t ↔ passageTime x f < t

Simultaneously at all levels and times, a strict infimum crossing occurs precisely when the corresponding strict passage time is before the observation time.