Theorems · Theorem

PMF.toMeasure_pure_apply

∀ {α : Type u_1} (a : α) (s : Set α) [inst : MeasurableSpace α],
  MeasurableSet s → (PMF.pure a).toMeasure s = if a ∈ s then 1 else 0

The measure of a set under pure a is 1 for sets containing a and 0 otherwise.

Defined in

Mathlib.Probability.ProbabilityMassFunction.Monad

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace