∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s t u : Set Ω},
  s.Finite →
    (ProbabilityTheory.uniformOn s) (t ∩ u) =
      (ProbabilityTheory.uniformOn (s ∩ u)) t * (ProbabilityTheory.uniformOn s) u