Theorems · Theorem · measure theory

MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [HasOuterApproxClosed Ω]
  [inst_3 : BorelSpace Ω], Function.Injective MeasureTheory.FiniteMeasure.toWeakDualBCNN

The mapping toWeakDualBCNN from finite Borel measures to the weak dual of Ω →ᵇ ℝ≥0 is injective, if in the underlying space Ω, indicator functions of closed sets have decreasing approximations by sequences of continuous functions (in particular if Ω is pseudometrizable).

Defined in

Mathlib.MeasureTheory.Measure.FiniteMeasure

Cited by

1 results in Mathlib

Foundations

Depth 222 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpaceHasOuterApproxClosedBorelSpace