LeanPool.RlTheoryInLean.MeasureTheory.Measure.GiryMonad

theorem MeasureTheory.Measure.ae_join_of_ae_ae {α : Type u_1} [MeasurableSpace α] {m : Measure (Measure α)} {p : α → Prop} (hp : MeasurableSet {a : α | p a}) (h : ∀ᵐ (μ : Measure α) ∂m, ∀ᵐ (a : α) ∂μ, p a) : ∀ᵐ (a : α) ∂m.join, p a

theorem MeasureTheory.Measure.ae_bind_of_ae_ae {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {m : Measure α} {p : β → Prop} {hp : MeasurableSet {a : β | p a}} {f : α → Measure β} (hf : AEMeasurable f m) (h : ∀ᵐ (a : α) ∂m, ∀ᵐ (b : β) ∂f a, p b) : ∀ᵐ (b : β) ∂m.bind f, p b