α : Type u_1
β : Type ?u.575084
γ : Type ?u.575087
δ : Type u_2
ι : Type ?u.575093
R : Type ?u.575096
R' : Type ?u.575099
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ ae (Measure.restrict μ s) ≤ ae μ
α : Type u_1
β : Type ?u.575084
γ : Type ?u.575087
δ : Type u_2
ι : Type ?u.575093
R : Type ?u.575096
R' : Type ?u.575099
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ f =ᶠ[ae (Measure.restrict μ s)] g
refine' hfg.filter_mono _
α : Type u_1
β : Type ?u.575084
γ : Type ?u.575087
δ : Type u_2
ι : Type ?u.575093
R : Type ?u.575096
R' : Type ?u.575099
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ Measure.restrict μ s ≪ μ
α : Type u_1
β : Type ?u.575084
γ : Type ?u.575087
δ : Type u_2
ι : Type ?u.575093
R : Type ?u.575096
R' : Type ?u.575099
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ ae (Measure.restrict μ s) ≤ ae μ
rw [Measure.ae_le_iff_absolutelyContinuous]
no goals
α : Type u_1
β : Type ?u.575084
γ : Type ?u.575087
δ : Type u_2
ι : Type ?u.575093
R : Type ?u.575096
R' : Type ?u.575099
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
f g : α → δ
s : Set α
hfg : f =ᶠ[ae μ] g
⊢ Measure.restrict μ s ≪ μ
exact Measure.absolutelyContinuous_of_le Measure.restrict_le_self