Finite products of measures without atoms

TODO: prove a version without topological assumptions.

theorem MeasureTheory.NoAtoms'.pi {ι : Type u_1} [Fintype ι] [Nonempty ι] {X : ι → Type u_2} [(i : ι) → MetricSpace (X i)] [∀ (i : ι), ProperSpace (X i)] [(i : ι) → MeasurableSpace (X i)] [∀ (i : ι), BorelSpace (X i)] (μ : (i : ι) → Measure (X i)) [∀ (i : ι), IsLocallyFiniteMeasure (μ i)] [∀ (i : ι), SigmaFinite (μ i)] [∀ (i : ι), NullSingletonClass (μ i)] : NoAtoms' (Measure.pi μ)

Analogue of MeasureTheory.Measure.pi_nullSingletonClass' for NoAtoms'.