Theorems · Theorem · probability

PMF.toOuterMeasure_uniformOfFintype_apply

∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] (s : Set α) [inst_2 : Fintype ↑s],
  (PMF.uniformOfFintype α).toOuterMeasure s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)

Defined in

Mathlib.Probability.Distributions.Uniform

Cited by

0 results in Mathlib

Foundations

Depth 145 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeNonemptyFintype