Theorems · Inductive type · measure theory
StieltjesFunction
(R : Type u_1) → [LinearOrder R] → [TopologicalSpace R] → Type u_1
Bundled monotone right-continuous real functions, used to construct Stieltjes measures.
- Defined in
- Mathlib.MeasureTheory.Measure.Stieltjes
- Cited by
- 85 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- LinearOrderTopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
- LinearOrderstatement · cited by 8,572
Cited by109
Results whose statement or proof uses this declaration.
- StieltjesFunction.toFunstatement and proof · cited by 120
- StieltjesFunction.measurestatement · cited by 48
- StieltjesFunction.monostatement and proof · cited by 23
- ProbabilityTheory.IsCondKernelCDFstatement · cited by 22
- ProbabilityTheory.stieltjesOfMeasurableRatstatement · cited by 22
- ProbabilityTheory.condCDFstatement · cited by 20
- ProbabilityTheory.cdfstatement · cited by 19
- StieltjesFunction.lengthstatement and proof · cited by 12
- ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionstatement · cited by 11
- ProbabilityTheory.IsCondKernelCDF.toKernelstatement and proof · cited by 9
- StieltjesFunction.idstatement · cited by 8
- StieltjesFunction.measure_Iccstatement and proof · cited by 8