ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type ?u.519115
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ ↑↑μ ({x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}ᶜ) = 0
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type ?u.519115
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ ↑↑μ (aeSeqSet hf pᶜ) = 0
rw [aeSeqSet, compl_compl, measure_toMeasurable]
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type ?u.519115
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
hf_eq : ∀ (i : ι), f i =ᵐ[μ] AEMeasurable.mk (f i) (_ : AEMeasurable (f i))
⊢ ↑↑μ ({x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}ᶜ) = 0
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type ?u.519115
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ ↑↑μ ({x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}ᶜ) = 0
have hf_eq := fun i => (hf i).ae_eq_mk
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type ?u.519115
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
hf_eq : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), f i a = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) a
⊢ ↑↑μ ({x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}ᶜ) = 0
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type ?u.519115
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
hf_eq : ∀ (i : ι), f i =ᵐ[μ] AEMeasurable.mk (f i) (_ : AEMeasurable (f i))
⊢ ↑↑μ ({x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}ᶜ) = 0
simp_rw [Filter.EventuallyEq, ← ae_all_iff] at hf_eq
no goals
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type ?u.519115
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
hf_eq : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), f i a = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) a
⊢ ↑↑μ ({x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) (_ : AEMeasurable (f i)) x) ∧ p x fun n => f n x}ᶜ) = 0
exact Filter.Eventually.and hf_eq hp