Theorems · Theorem · measure theory

MeasureTheory.restrict_dirac

∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} {a : α} [MeasurableSingletonClass α]
  [inst_2 : Decidable (a ∈ s)],
  (MeasureTheory.Measure.dirac a).restrict s = if a ∈ s then MeasureTheory.Measure.dirac a else 0

Defined in

Mathlib.MeasureTheory.Measure.Dirac

Cited by

2 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSingletonClassDecidable