Theorems · Theorem · measure theory
StieltjesFunction.ext
∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] {f g : StieltjesFunction R},
(∀ (x : R), ↑f x = ↑g x) → f = g- Defined in
- Mathlib.MeasureTheory.Measure.Stieltjes
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 122 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LinearOrderTopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- TopologicalSpacestatement and proof · cited by 24,529
- LinearOrderstatement and proof · cited by 8,572
- StieltjesFunction.toFunstatement and proof · cited by 120
- StieltjesFunctionstatement and proof · cited by 85
- StieltjesFunction.mono'proof · cited by 4
- StieltjesFunction.right_continuous'proof · cited by 3
- StieltjesFunction.mk.injEqproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- ProbabilityTheory.condCDF_eq_stieltjesOfMeasurableRat_unit_prodproof · cited by 2
- StieltjesFunction.eq_of_measure_of_tendsto_atBotproof · cited by 1
- StieltjesFunction.ext_iffproof · cited by 0
- StieltjesFunction.eq_of_measure_of_eqproof · cited by 0