Theorems · Theorem · measure theory

MeasureTheory.Measure.map_dirac

∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [MeasurableSingletonClass α]
  [MeasurableSingletonClass β] {f : α → β} (a : α),
  MeasureTheory.Measure.map f (MeasureTheory.Measure.dirac a) = MeasureTheory.Measure.dirac (f a)

Defined in: Mathlib.MeasureTheory.Measure.Dirac
Cited by: 7 results in Mathlib
Foundations: Depth 199 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace MeasurableSpace MeasurableSingletonClass MeasurableSingletonClass

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites15

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Setproof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement · cited by 10,939
ENNRealproof · cited by 9,879
Set.preimageproof · cited by 4,946
MeasurableSetproof · cited by 3,075
MeasureTheory.Measure.mapstatement · cited by 858
MeasureTheory.Measure.extproof · cited by 308
MeasurableSingletonClassstatement and proof · cited by 230
MeasureTheory.Measure.diracstatement and proof · cited by 210
Set.indicator_applyproof · cited by 48

Cited by7

Results whose statement or proof uses this declaration.

ProbabilityTheory.gaussianReal_map_const_mulproof · cited by 4
ProbabilityTheory.gaussianReal_map_add_constproof · cited by 3
ProbabilityTheory.map_cast_binomial_eq_sum_diracproof · cited by 1
ProbabilityTheory.binomial_zeroproof · cited by 0
ProbabilityTheory.map_cast_binomial_zeroproof · cited by 0
volume_euclideanSpace_eq_diracproof · cited by 0
ProbabilityTheory.map_bernoulliMeasureproof · cited by 0