α : Type u_1
β : Type ?u.576111
γ : Type ?u.576114
δ : Type ?u.576117
ι : Type ?u.576120
R : Type ?u.576123
R' : Type ?u.576126
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
hs : NullMeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → p x
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, p x
α : Type u_1
β : Type ?u.576111
γ : Type ?u.576114
δ : Type ?u.576117
ι : Type ?u.576120
R : Type ?u.576123
R' : Type ?u.576126
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
hs : NullMeasurableSet s
⊢ (∀ᵐ (x : α) ∂Measure.restrict μ s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x
refine' ⟨fun h => ae_imp_of_ae_restrict h, fun h => _⟩
no goals
α : Type u_1
β : Type ?u.576111
γ : Type ?u.576114
δ : Type ?u.576117
ι : Type ?u.576120
R : Type ?u.576123
R' : Type ?u.576126
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
p : α → Prop
hs : NullMeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → p x
⊢ ∀ᵐ (x : α) ∂Measure.restrict μ s, p x
filter_upwards [ae_restrict_mem₀ hs, ae_restrict_of_ae h]with x hx h'x using h'x hx