ι : Sort u_2
α : Type u_3
β : Type u_1
γ : Type ?u.727906
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ ↑↑μ {a | ¬(⨆ (i : ι), aeSeq hf p i a) = ⨆ (i : ι), f i a} = 0
ι : Sort u_2
α : Type u_3
β : Type u_1
γ : Type ?u.727906
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ (⨆ (n : ι), aeSeq hf p n) =ᵐ[μ] ⨆ (n : ι), f n
simp_rw [Filter.EventuallyEq, ae_iff, iSup_apply]
ι : Sort u_2
α : Type u_3
β : Type u_1
γ : Type ?u.727906
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
h_ss : aeSeqSet hf p ⊆ {a | (⨆ (i : ι), aeSeq hf p i a) = ⨆ (i : ι), f i a}
⊢ ↑↑μ {a | ¬(⨆ (i : ι), aeSeq hf p i a) = ⨆ (i : ι), f i a} = 0
ι : Sort u_2
α : Type u_3
β : Type u_1
γ : Type ?u.727906
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ ↑↑μ {a | ¬(⨆ (i : ι), aeSeq hf p i a) = ⨆ (i : ι), f i a} = 0
have h_ss : aeSeqSet hf p ⊆ { a : α | (⨆ i : ι, aeSeq hf p i a) = ⨆ i : ι, f i a } := by
  intro x hx
  congr
  exact funext fun i => aeSeq_eq_fun_of_mem_aeSeqSet hf hx i
no goals
ι : Sort u_2
α : Type u_3
β : Type u_1
γ : Type ?u.727906
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
h_ss : aeSeqSet hf p ⊆ {a | (⨆ (i : ι), aeSeq hf p i a) = ⨆ (i : ι), f i a}
⊢ ↑↑μ {a | ¬(⨆ (i : ι), aeSeq hf p i a) = ⨆ (i : ι), f i a} = 0
exact measure_mono_null (Set.compl_subset_compl.mpr h_ss) (measure_compl_aeSeqSet_eq_zero hf hp)
ι : Sort u_2
α : Type u_3
β : Type u_1
γ : Type ?u.727906
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
x : α
hx : x ∈ aeSeqSet hf p
⊢ x ∈ {a | (⨆ (i : ι), aeSeq hf p i a) = ⨆ (i : ι), f i a}
ι : Sort u_2
α : Type u_3
β : Type u_1
γ : Type ?u.727906
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
⊢ aeSeqSet hf p ⊆ {a | (⨆ (i : ι), aeSeq hf p i a) = ⨆ (i : ι), f i a}
intro x hx
case e_s
ι : Sort u_2
α : Type u_3
β : Type u_1
γ : Type ?u.727906
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
x : α
hx : x ∈ aeSeqSet hf p
⊢ (fun i => aeSeq hf p i x) = fun i => f i x
ι : Sort u_2
α : Type u_3
β : Type u_1
γ : Type ?u.727906
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
x : α
hx : x ∈ aeSeqSet hf p
⊢ x ∈ {a | (⨆ (i : ι), aeSeq hf p i a) = ⨆ (i : ι), f i a}
congr
no goals
case e_s
ι : Sort u_2
α : Type u_3
β : Type u_1
γ : Type ?u.727906
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
f : ι → α → β
μ : MeasureTheory.Measure α
p : α → (ι → β) → Prop
inst✝¹ : CompleteLattice β
inst✝ : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i)
hp : ∀ᵐ (x : α) ∂μ, p x fun n => f n x
x : α
hx : x ∈ aeSeqSet hf p
⊢ (fun i => aeSeq hf p i x) = fun i => f i x
exact funext fun i => aeSeq_eq_fun_of_mem_aeSeqSet hf hx i