instMetrizableSpaceProbabilityMeasure

English

The homeomorphism structure is defined by a pair of continuous maps between ProbabilityMeasure Ω and LevyProkhorov(ProbabilityMeasure Ω).

Русский

Структура гомеоморфизма задаётся парами непрерывных отображений между ProbabilityMeasure Ω и LevyProkhorov(ProbabilityMeasure Ω).

LaTeX

$$$\\mathrm{homeomorph\\_probabilityMeasure\\_levyProkhorov}$ is a definition of a homeomorphism with explicit toFun and invFun.$$

Lean4

/-- The topology of convergence in distribution on a separable Borel space is metrizable. -/
instance instMetrizableSpaceProbabilityMeasure (X : Type*) [TopologicalSpace X] [PseudoMetrizableSpace X]
    [SeparableSpace X] [MeasurableSpace X] [BorelSpace X] : MetrizableSpace (ProbabilityMeasure X) :=
  by
  letI : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
  exact homeomorph_probabilityMeasure_levyProkhorov.isEmbedding.metrizableSpace

Похожие утверждения