Theorems · Definition · measure theory
MeasureTheory.diracProba
{X : Type u_1} → [inst : MeasurableSpace X] → X → MeasureTheory.ProbabilityMeasure XThe Dirac delta mass at a point x : X as a ProbabilityMeasure.
- Defined in
- Mathlib.MeasureTheory.Measure.DiracProba
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measure.diracproof · cited by 210
- MeasureTheory.ProbabilityMeasurestatement · cited by 127
Cited by18
Results whose statement or proof uses this declaration.
- MeasureTheory.diracProbaEquivstatement and proof · cited by 5
- MeasureTheory.continuous_diracProbastatement · cited by 2
- MeasureTheory.diracProbaInversestatement and proof · cited by 2
- MeasureTheory.diracProbaHomeomorphstatement · cited by 1
- MeasureTheory.diracProba_comp_diracProbaEquiv_symm_eq_valstatement and proof · cited by 1
- MeasureTheory.diracProba_diracProbaInversestatement and proof · cited by 1
- MeasureTheory.tendsto_diracProbaEquivSymm_iff_tendstostatement and proof · cited by 1
- MeasureTheory.tendsto_diracProba_iff_tendstostatement and proof · cited by 1
- MeasureTheory.not_tendsto_diracProba_of_not_tendstostatement · cited by 1
- MeasureTheory.injective_diracProbastatement and proof · cited by 1
- MeasureTheory.continuous_diracProbaEquivstatement · cited by 0
- MeasureTheory.continuous_diracProbaEquivSymmstatement and proof · cited by 0