instTopologicalSpace — Mathlib

English

The topology on FiniteMeasure Ω is the one induced by the map toWeakDualBCNN.

Русский

Топология на FiniteMeasure Ω индуцирована отображением в toWeakDualBCNN.

LaTeX

$$$ \text{TopologicalSpace}(\text{FiniteMeasure } \Omega) \\ = \text{TopologicalSpace.induced}(\text{toWeakDualBCNN}, \text{FiniteMeasure } \Omega). $$$

Lean4

/-- The topology of weak convergence on `MeasureTheory.FiniteMeasure Ω` is inherited (induced)
from the weak-* topology on `WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0)` via the function
`MeasureTheory.FiniteMeasure.toWeakDualBCNN`. -/
instance instTopologicalSpace : TopologicalSpace (FiniteMeasure Ω) :=
  TopologicalSpace.induced toWeakDualBCNN inferInstance

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