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

theorem ProbabilityTheory.real_uniformOn_apply_singleton_of_mem {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} {x : Ω} (hx : x ∈ s) (hs : s.Finite) : (uniformOn s).real {x} = 1 / ↑(Nat.card ↑s)

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

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

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

theorem ProbabilityTheory.uniformOn_of_infinite {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : s.Infinite) : uniformOn s = 0

theorem ProbabilityTheory.uniformOn_apply {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : s.Finite) (t : Set Ω) : (uniformOn s) t = ↑(Nat.card ↑(s ∩ t)) / ↑(Nat.card ↑s)

theorem ProbabilityTheory.uniformOn_real {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : s.Finite) (t : Set Ω) : (uniformOn s).real t = ↑(Nat.card ↑(s ∩ t)) / ↑(Nat.card ↑s)

theorem ProbabilityTheory.uniformOn_real_singleton {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} (hs : s.Finite) (ω : Ω) [Decidable (ω ∈ s)] : (uniformOn s).real {ω} = if ω ∈ s then (↑s.ncard)⁻¹ else 0

instance ProbabilityTheory.uniformOn.instIsProbabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω} [Nonempty ↑s] [Finite ↑s] : MeasureTheory.IsProbabilityMeasure (uniformOn s)

theorem ProbabilityTheory.map_uniformOn_apply {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [MeasurableSpace Ω'] [MeasurableSingletonClass Ω'] {s : Set Ω} {f : Ω → Ω'} (hmes : Measurable f) (hf : Function.Injective f) {t : Set Ω'} (ht : MeasurableSet t) : (MeasureTheory.Measure.map f (uniformOn s)) t = (uniformOn (f '' s)) t

theorem ProbabilityTheory.map_uniformOn {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSingletonClass Ω] [MeasurableSpace Ω'] [MeasurableSingletonClass Ω'] {s : Set Ω} {f : Ω → Ω'} (hmes : Measurable f) (hf : Function.Injective f) : MeasureTheory.Measure.map f (uniformOn s) = uniformOn (f '' s)