Theorems · Theorem · probability

MeasureTheory.LevyProkhorov.continuous_toMeasure_probabilityMeasure

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoMetricSpace Ω] [inst_2 : OpensMeasurableSpace Ω],
  Continuous MeasureTheory.LevyProkhorov.toMeasure

The identity map LevyProkhorov (ProbabilityMeasure Ω) → ProbabilityMeasure Ω is continuous.

Defined in: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Cited by: 1 results in Mathlib
Foundations: Depth 268 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace PseudoMetricSpace OpensMeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites90

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

DFunLike.coeproof · cited by 62,936
Realproof · cited by 25,697
MeasurableSpacestatement and proof · cited by 13,106
ENNRealproof · cited by 9,879
Top.topproof · cited by 9,680
Set.ofPredproof · cited by 6,101
nhdsproof · cited by 5,554
Norm.normproof · cited by 5,413
Set.preimageproof · cited by 4,946
mul_oneproof · cited by 3,885
Filter.Tendstoproof · cited by 3,814
one_mulproof · cited by 2,841

Cited by2

Results whose statement or proof uses this declaration.

MeasureTheory.LevyProkhorov.le_convergenceInDistributionproof · cited by 1
MeasureTheory.LevyProkhorov.probabilityMeasureHomeomorphproof · cited by 0