Structures · Analysis
BorelSpace
A space with MeasurableSpace and TopologicalSpace structures such that
the σ-algebra of measurable sets is exactly the σ-algebra generated by open sets.
- Shape
- One type argument · adds measurable_eq
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances22
- Int
- Nat
- Real
- Rat
- Bool
- Complex
- NNReal
- ContinuousLinearMap
- ENNReal
- WithLp
- EReal
- Empty
- PiLp
- UpperHalfPlane
- Subtype
- Prod
- OrderDual
- ULift
- HasQuotient.Quotient
- WithTop
- Quotient
- Unit
How is a type an instance?
Loading the hierarchy index…
Assumed by1,835
- Continuous.measurable
- MeasureTheory.StronglyMeasurable.measurable
- MeasureTheory.AEStronglyMeasurable.aemeasurable
- MeasureTheory.Measure.hausdorffMeasure
- MeasureTheory.Measure.addHaarScalarFactor
- StieltjesFunction.measure
- Homeomorph.toMeasurableEquiv
- MeasureTheory.Measure.haarScalarFactor
- BorelSpace.measurable_eq
- MeasureTheory.Measure.addHaar
- ProbabilityTheory.covarianceBilin
- ContinuousLinearMap.measurable
- ProbabilityTheory.covarianceBilinDual
- Continuous.aemeasurable
- MeasureTheory.Measure.euclideanHausdorffMeasure
- MeasureTheory.Measure.addHaarMeasure
- Homeomorph.measurableEmbedding
- ContinuousMap.toLp
- MeasureTheory.Lp.toTemperedDistribution
- Topology.IsClosedEmbedding.measurableEmbedding
- TemperedDistribution.MemSobolev
- TemperedDistribution.fourierMultiplierCLM
- TemperedDistribution.besselPotential
- ProbabilityTheory.HasGaussianLaw.map
- Module.Basis.addHaar
- SchwartzMap.toTemperedDistributionCLM
- Measurable.iSup
- ProbabilityTheory.HasGaussianLaw.memLp_two
- MeasureTheory.Measure.addHaar_smul
- stronglyMeasurable_iff_measurable_separable
- IsUnifLocDoublingMeasure.vitaliFamily
- SchwartzMap.fourierMultiplierCLM
- BoundedContinuousFunction.toLp
- MeasureTheory.mulEquivHaarChar
- MeasureTheory.Measure.haar
- MeasureTheory.addEquivAddHaarChar
- VitaliFamily.limRatioMeas
- ProbabilityTheory.IsGaussian.integrable_id
- BoundedVariationOn.vectorMeasure
- ExistsContDiffBumpBase.w
- MeasureTheory.Integrable.aemeasurable
- MeasureTheory.Measure.haarMeasure
- MeasureTheory.MemLp.aemeasurable
- aestronglyMeasurable_iff_aemeasurable_separable
- MeasureTheory.Measure.euclideanHausdorffMeasure_def
- IsCompact.measure_closure
- MeasureTheory.Content.measure
- MeasureTheory.Measure.mkMetric
- SchwartzMap.integrable
- ProbabilityTheory.IsGaussian.memLp_two_id
Ancestors0
No ancestors.