Theorems · Definition · measure theory

MeasureTheory.FiniteMeasure.toWeakDualBCNN

{Ω : Type u_1} →
  [inst : MeasurableSpace Ω] →
    [inst_1 : TopologicalSpace Ω] →
      [OpensMeasurableSpace Ω] → MeasureTheory.FiniteMeasure Ω → WeakDual NNReal (BoundedContinuousFunction Ω NNReal)

Finite measures yield elements of the WeakDual of bounded continuous nonnegative functions via MeasureTheory.FiniteMeasure.testAgainstNN, i.e., integration.

Defined in: Mathlib.MeasureTheory.Measure.FiniteMeasure
Cited by: 8 results in Mathlib
Foundations: Depth 209 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace TopologicalSpace OpensMeasurableSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites9

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

TopologicalSpacestatement and proof · cited by 24,529
MeasurableSpacestatement and proof · cited by 13,106
NNRealstatement and proof · cited by 4,310
OpensMeasurableSpacestatement and proof · cited by 636
BoundedContinuousFunctionstatement and proof · cited by 511
MeasureTheory.FiniteMeasurestatement and proof · cited by 150
WeakDualstatement · cited by 103
MeasureTheory.FiniteMeasure.testAgainstNNproof · cited by 27
MeasureTheory.FiniteMeasure.testAgainstNN_addproof · cited by 0

Cited by9

Results whose statement or proof uses this declaration.

MeasureTheory.ProbabilityMeasure.toWeakDualBCNNproof · cited by 3
MeasureTheory.FiniteMeasure.toWeakDualBCNN_continuousstatement · cited by 2
MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendstostatement and proof · cited by 2
MeasureTheory.FiniteMeasure.toWeakDualBCNN_applystatement · cited by 1
MeasureTheory.FiniteMeasure.injective_toWeakDualBCNNstatement and proof · cited by 1
MeasureTheory.FiniteMeasure.tendsto_iff_weakDual_tendstostatement · cited by 1
MeasureTheory.FiniteMeasure.toWeakDualBCNN.congr_simpstatement and proof · cited by 0
MeasureTheory.FiniteMeasure.coe_toWeakDualBCNNstatement · cited by 0
MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNNstatement · cited by 0