Theorems · Definition · measure theory
borel
(α : Type u) → [TopologicalSpace α] → MeasurableSpace α
MeasurableSpace structure generated by TopologicalSpace.
- Cited by
- 57 results in Mathlib
- Foundations
- Depth 8 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- MeasurableSpacestatement · cited by 13,106
- Set.ofPredproof · cited by 6,101
- IsOpenproof · cited by 2,400
- MeasurableSpace.generateFromproof · cited by 172
Cited by63
Results whose statement or proof uses this declaration.
- BorelSpace.measurable_eqstatement · cited by 26
- MeasureTheory.Measure.measurable_of_measurable_coeproof · cited by 9
- borel_eq_generateFrom_Iiostatement · cited by 6
- dimH_defproof · cited by 5
- borel_eq_generateFrom_Ioistatement · cited by 5
- OpensMeasurableSpace.borel_lestatement · cited by 4
- borel_eq_generateFrom_Iicstatement · cited by 4
- Continuous.borel_measurablestatement · cited by 3
- Dense.borel_eq_generateFrom_Ico_mem_auxstatement and proof · cited by 3
- MeasureTheory.Measure.addModularCharacterFun_eq_addHaarScalarFactorproof · cited by 3
- MeasureTheory.Measure.modularCharacterFun_eq_haarScalarFactorproof · cited by 3
- MeasureTheory.measure_le_eq_ltproof · cited by 3