Theorems · Definition · measure theory

MeasureTheory.diracProbaEquiv

{X : Type u_1} →
  [inst : MeasurableSpace X] →
    [inst_1 : TopologicalSpace X] → [OpensMeasurableSpace X] → [T0Space X] → X ≃ ↑(Set.range MeasureTheory.diracProba)

In a T0 topological space X, the assignment x ↦ diracProba x is a bijection to its range in ProbabilityMeasure X.

Defined in: Mathlib.MeasureTheory.Measure.DiracProba
Cited by: 5 results in Mathlib
Foundations: Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace TopologicalSpace OpensMeasurableSpace T0Space

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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

TopologicalSpacestatement and proof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
Equivstatement · cited by 8,337
Set.Elemstatement · cited by 7,166
Set.rangestatement · cited by 4,705
OpensMeasurableSpacestatement and proof · cited by 636
T0Spacestatement and proof · cited by 179
MeasureTheory.ProbabilityMeasurestatement · cited by 127
MeasureTheory.diracProbastatement and proof · cited by 15
MeasureTheory.diracProbaInverseproof · cited by 2

Cited by6

Results whose statement or proof uses this declaration.

MeasureTheory.tendsto_diracProbaEquivSymm_iff_tendstostatement and proof · cited by 1
MeasureTheory.diracProbaHomeomorphproof · cited by 1
MeasureTheory.diracProba_comp_diracProbaEquiv_symm_eq_valstatement · cited by 1
MeasureTheory.continuous_diracProbaEquivstatement · cited by 0
MeasureTheory.continuous_diracProbaEquivSymmstatement · cited by 0
MeasureTheory.diracProbaEquiv.congr_simpstatement and proof · cited by 0