theorem ProbabilityTheory.uniformOn_apply_singleton_of_mem {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {A : Set Ω} {x : Ω} (hx : x ∈ A) (h'A : A.Finite) : (ProbabilityTheory.uniformOn A) {x} = 1 / ↑(Nat.card ↑A)

theorem ProbabilityTheory.uniformOn_apply_singleton_of_nmem {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {A : Set Ω} {x : Ω} (hx : x ∉ A) : (ProbabilityTheory.uniformOn A) {x} = 0

theorem ProbabilityTheory.uniformOn_apply_eq_zero {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} {t : Set Ω} (hst : s ∩ t = ∅) : (ProbabilityTheory.uniformOn s) t = 0