instTopologicalSpace — Mathlib

English

The weak topology on ProbabilityMeasure Ω is the topology induced from the weak topology of FiniteMeasure via the map toFiniteMeasure.

Русский

Слабая топология на ProbabilityMeasure Ω является топологией, индуцированной отображением кFiniteMeasure из слабой топологии конечных мер.

LaTeX

$$$\\text{TopologicalSpace}(\\text{ProbabilityMeasure } \\Omega) = \\text{TopologicalSpace.induced}(\\text{toFiniteMeasure})$$$

Lean4

/-- The topology of weak convergence on `MeasureTheory.ProbabilityMeasure Ω`. This is inherited
(induced) from the topology of weak convergence of finite measures via the inclusion
`MeasureTheory.ProbabilityMeasure.toFiniteMeasure`. -/
instance : TopologicalSpace (ProbabilityMeasure Ω) :=
  TopologicalSpace.induced toFiniteMeasure inferInstance

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