Theorems · Definition · measure theory
rieszContent
{X : Type u_1} →
[inst : TopologicalSpace X] →
[T2Space X] →
[LocallyCompactSpace X] → (CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal) → MeasureTheory.Content XThe content induced by the linear functional Λ.
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
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
- RingHom.idstatement and proof · cited by 18,349
- LinearMapstatement and proof · cited by 10,215
- SetLike.coeproof · cited by 8,199
- NNRealstatement and proof · cited by 4,310
- Disjointproof · cited by 2,201
- IsClosedproof · cited by 1,639
- T2Spacestatement and proof · cited by 1,351
- TopologicalSpace.Compactsproof · cited by 386
- LocallyCompactSpacestatement and proof · cited by 324
- CompactlySupportedContinuousMapstatement and proof · cited by 134
- MeasureTheory.Contentstatement · cited by 60
Cited by9
Results whose statement or proof uses this declaration.
- RealRMK.rieszMeasureproof · cited by 8
- NNRealRMK.rieszMeasureproof · cited by 7
- NNRealRMK.integral_rieszMeasureproof · cited by 3
- RealRMK.rieszMeasure_le_of_eq_oneproof · cited by 3
- contentRegular_rieszContentstatement · cited by 3
- NNRealRMK.le_rieszMeasure_of_isCompact_tsupport_subsetproof · cited by 1
- rieszContent.congr_simpstatement and proof · cited by 1
- rieszContent_ne_topstatement · cited by 0
- RealRMK.le_rieszMeasure_tsupport_subsetproof · cited by 0