Theorems · Theorem · probability

ProbabilityTheory.setBernoulli_singleton

∀ {ι : Type u_1} {s u : Set ι} (p : ↑unitInterval) [Countable ι],
  s ⊆ u →
    u.Finite →
      (ProbabilityTheory.setBernoulli u p) {s} =
        ↑(unitInterval.toNNReal p) ^ s.ncard * ↑(unitInterval.toNNReal (unitInterval.symm p)) ^ (u \ s).ncard

Defined in

Mathlib.Probability.Distributions.SetBernoulli

Cited by

3 results in Mathlib

Foundations

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

Assumes

Countable