Theorems · Inductive type · measure theory
BorelSpace
(α : Type u_6) → [TopologicalSpace α] → [MeasurableSpace α] → Prop
A space with MeasurableSpace and TopologicalSpace structures such that
the σ-algebra of measurable sets is exactly the σ-algebra generated by open sets.
- Cited by
- 1,602 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 3 definitions · uses no axioms
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
- MeasurableSpacestatement · cited by 13,106
Cited by1,684
Results whose statement or proof uses this declaration.
- Continuous.measurablestatement and proof · cited by 181
- MeasureTheory.StronglyMeasurable.measurablestatement and proof · cited by 74
- MeasureTheory.AEStronglyMeasurable.aemeasurablestatement and proof · cited by 73
- MeasureTheory.Measure.hausdorffMeasurestatement and proof · cited by 71
- MeasureTheory.Measure.addHaarScalarFactorstatement and proof · cited by 58
- StieltjesFunction.measurestatement · cited by 48
- Homeomorph.toMeasurableEquivstatement and proof · cited by 32
- MeasureTheory.Measure.haarScalarFactorstatement and proof · cited by 31
- MeasureTheory.Measure.addHaarstatement and proof · cited by 26
- BorelSpace.measurable_eqstatement and proof · cited by 26
- ProbabilityTheory.covarianceBilinstatement and proof · cited by 25
- ContinuousLinearMap.measurablestatement and proof · cited by 22
Showing the 200 most cited of 1,684.