exact Filter.eventually_of_forall h
α : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : LE E
f g : α → E
s : Set α
hs : MeasurableSet s
μ : Measure α
h : ∀ x ∈ s, f x ≤ g x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → f x ≤ g x
no goals