Theorem: Filter_eventuallyLe_restrict_of_forall_mem_imp (ForML/IntegralMeanValue.lean)

State before:
α : 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
⊢ f ≤ᵐ[Measure.restrict μ s] g
Tactic:
rw [Filter.EventuallyLE]
State after:
α : 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 : α) ∂Measure.restrict μ s, f x ≤ g x

State before:
α : 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 : α) ∂Measure.restrict μ s, f x ≤ g x
Tactic:
rw [ae_restrict_iff' hs]
State after:
α : 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

State before:
α : 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
Tactic:
exact Filter.eventually_of_forall h
State after:
no goals