no goals
α : Type u_1
β : Type ?u.293210
E : Type ?u.293213
F : Type ?u.293216
inst✝ : MeasurableSpace α
μ : Measure α
f : α → ℝ
s : Set α
hs : MeasurableSet s
hf : ∀ᵐ (a : α) ∂μ, a ∈ s → 0 ≤ f a
⊢ 0 ≤ᵐ[Measure.restrict μ s] fun a => f a
rwa [EventuallyLE, ae_restrict_iff' hs]