ι : Type ?u.1320516
α : Type u_1
β : Type u_2
γ : Type ?u.1320525
δ : Type ?u.1320528
R : Type ?u.1320531
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
⊢ AEMeasurable f ∧ AEMeasurable f ↔ AEMeasurable f ∧ AEMeasurable f
ι : Type ?u.1320516
α : Type u_1
β : Type u_2
γ : Type ?u.1320525
δ : Type ?u.1320528
R : Type ?u.1320531
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
⊢ AEMeasurable f ↔ AEMeasurable f ∧ AEMeasurable f
rw [← sum_cond, aemeasurable_sum_measure_iff, Bool.forall_bool, and_comm]
no goals
ι : Type ?u.1320516
α : Type u_1
β : Type u_2
γ : Type ?u.1320525
δ : Type ?u.1320528
R : Type ?u.1320531
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g : α → β
μ ν : MeasureTheory.Measure α
⊢ AEMeasurable f ∧ AEMeasurable f ↔ AEMeasurable f ∧ AEMeasurable f
rfl