Structures · Analysis
MeasurableSpace
A measurable space is a space equipped with a σ-algebra.
- Shape
- One type argument · adds MeasurableSet', measurableSet_empty, measurableSet_compl, measurableSet_iUnion
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by3
Forgetful instances
Provided automatically by
Concrete types that are instances44
- Int
- Nat
- Real
- Rat
- Bool
- Complex
- NNReal
- ContinuousLinearMap
- ZMod
- ENNReal
- ENat
- Units
- WithLp
- EReal
- AddUnits
- Empty
- AddChar
- SimpleGraph
- MeasureTheory.Measure
- UpperHalfPlane
- MeasureTheory.FiniteMeasure
- MeasureTheory.NullMeasurableSpace
- IterateMulAct
- IterateAddAct
- MeasureTheory.ProbabilityMeasure
- List.TProd
- SFinKer.carrier
- MeasCat.carrier
- Subtype
- Prod
- OrderDual
- ULift
- MulOpposite
- Fin
- PUnit
- AddOpposite
- HasQuotient.Quotient
- WithTop
- Sum
- Sigma
- Set
- Finset
- Quotient
- Quot
How is a type an instance?
Loading the hierarchy index…
Assumed by6,195
- MeasurableSet
- Measurable
- MeasureTheory.Measure.map
- MeasureTheory.AEEqFun
- AEMeasurable
- MeasureTheory.AEStronglyMeasurable
- MeasureTheory.AEEqFun.cast
- MeasureTheory.StronglyMeasurable
- MeasureTheory.Measure.prod
- MeasureTheory.NullMeasurableSet
- Measurable.aemeasurable
- MeasureTheory.Measure.dirac
- ProbabilityTheory.IndepFun
- Continuous.measurable
- MeasurableEquiv.symm
- MeasureTheory.FiniteMeasure
- ProbabilityTheory.iIndepFun
- MeasureTheory.Measure.pi
- MeasureTheory.ProbabilityMeasure
- MeasureTheory.Lp.simpleFunc
- MeasureTheory.SignedMeasure
- Measurable.comp_aemeasurable
- MeasureTheory.SimpleFunc.range
- MeasureTheory.Measure.comap
- ProbabilityTheory.Kernel.const
- MeasureTheory.LocallyIntegrable
- MeasureTheory.FiniteMeasure.toMeasure
- ProbabilityTheory.Kernel.map
- IsOpen.measurableSet
- MeasureTheory.LocallyIntegrableOn
- MeasureTheory.ProbabilityMeasure.toMeasure
- MeasureTheory.toMeasurable
- measurable_pi_apply
- MeasureTheory.Measure.toOuterMeasure
- MeasureTheory.StronglyMeasurable.measurable
- MeasureTheory.AEStronglyMeasurable.aemeasurable
- MeasureTheory.MeasurePreserving.map_eq
- MeasureTheory.Measure.hausdorffMeasure
- MeasureTheory.Measure.fst
- ProbabilityTheory.Kernel.IndepFun
- MeasureTheory.integral_map
- AEMeasurable.ae_eq_mk
- MeasureTheory.convolution
- IsClosed.measurableSet
- ProbabilityTheory.Kernel.iIndepFun
- MeasureTheory.measurableSet_toMeasurable
- AEMeasurable.measurable_mk
- MeasurableEquiv.measurableEmbedding
- MeasureTheory.Measure.count
- Measurable.aestronglyMeasurable
Ancestors0
No ancestors.