Documentation
SphereEversion
.
ToMathlib
.
MeasureTheory
.
BorelSpace
Search
return to top
source
Imports
Init
Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Imported by
borelSpace_borel
source
theorem
borelSpace_borel
(
X
:
Type
u_1)
[
TopologicalSpace
X
]
:
BorelSpace
X