theorem MeasureTheory.IsProjectiveMeasureFamily.empty {ι : Type u_1} {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] {P : (J : Finset ι) → MeasureTheory.Measure ((j : { x : ι // x ∈ J }) → α ↑j)} (hP : MeasureTheory.IsProjectiveMeasureFamily P) (h : ∃ (i : ι), IsEmpty (α i)) (I : Finset ι) : P I = 0