α : Type u_1
β : Type ?u.319127
γ : Type ?u.319130
δ : Type ?u.319133
ι : Type ?u.319136
R : Type ?u.319139
R' : Type ?u.319142
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : ∃ᵐ (a : α) ∂restrict μ s, a ∈ s
p : α → Prop
hp : ∀ᵐ (x : α) ∂restrict μ s, p x
⊢ ∃ x, x ∈ s ∧ p x
α : Type u_1
β : Type ?u.319127
γ : Type ?u.319130
δ : Type ?u.319133
ι : Type ?u.319136
R : Type ?u.319139
R' : Type ?u.319142
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : ↑↑μ s ≠ 0
p : α → Prop
hp : ∀ᵐ (x : α) ∂restrict μ s, p x
⊢ ∃ x, x ∈ s ∧ p x
rw [← μ.restrict_apply_self, ← frequently_ae_mem_iff] at hs
no goals
α : Type u_1
β : Type ?u.319127
γ : Type ?u.319130
δ : Type ?u.319133
ι : Type ?u.319136
R : Type ?u.319139
R' : Type ?u.319142
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : ∃ᵐ (a : α) ∂restrict μ s, a ∈ s
p : α → Prop
hp : ∀ᵐ (x : α) ∂restrict μ s, p x
⊢ ∃ x, x ∈ s ∧ p x
exact (hs.and_eventually hp).exists