Theorems · Definition · general topology
upgradeStandardBorel
(α : Type u_1) → [inst : MeasurableSpace α] → [h : StandardBorelSpace α] → UpgradedStandardBorel α
Use as letI := upgradeStandardBorel α to endow a standard Borel space α with
a compatible Polish topology.
Warning: following this with borelize α will cause an error. Instead, one can
rewrite with eq_borel_upgradeStandardBorel α.
TODO: fix the corresponding bug in borelize.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpaceproof · cited by 24,529
- MeasurableSpacestatement and proof · cited by 13,106
- BorelSpaceproof · cited by 1,602
- StandardBorelSpacestatement and proof · cited by 304
- PolishSpaceproof · cited by 57
- UpgradedStandardBorelstatement · cited by 4
- StandardBorelSpace.polishproof · cited by 0
Cited by5
Results whose statement or proof uses this declaration.
- eq_borel_upgradeStandardBorelstatement · cited by 3
- MeasurableSet.image_of_measurable_injOnproof · cited by 1
- MeasurableSet.analyticSet_imageproof · cited by 1
- MeasurableSet.isClopenable'proof · cited by 1
- Measurable.exists_eq_measurable_compproof · cited by 0