Structures · Analysis
MeasurableSingletonClass
A typeclass mixin for MeasurableSpaces such that each singleton is measurable.
- Shape
- One type argument · adds measurableSet_singleton
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances12
- Int
- Nat
- Rat
- Bool
- ZMod
- ENat
- MeasureTheory.NullMeasurableSpace
- Subtype
- Prod
- Fin
- Set
- Finset
How is a type an instance?
Loading the hierarchy index…
Assumed by246
- MeasurableSingletonClass.measurableSet_singleton
- MeasureTheory.ae_dirac_eq
- MeasureTheory.integral_dirac
- MeasurableSet.singleton
- Set.Finite.measurableSet
- Set.Countable.measurableSet
- MeasureTheory.lintegral_dirac
- MeasureTheory.Measure.dirac_apply
- MeasureTheory.integrableOn_singleton
- integrableOn_Icc_iff_integrableOn_Ioc
- MeasureTheory.Measure.map_dirac
- integrableOn_Ici_iff_integrableOn_Ioi
- measurable_from_prod_countable_left
- MeasureTheory.Measure.toPMF
- MeasureTheory.AEStronglyMeasurable.of_discrete
- aemeasurable_indicator_const_iff
- measurableSet_support
- MeasureTheory.ae_eq_dirac
- MeasureTheory.nullMeasurableSet_singleton
- measurableSet_eq
- MeasureTheory.Measure.count_apply_lt_top
- measurable_of_measurable_on_compl_singleton
- measurable_indicator_const_iff
- MeasureTheory.lintegral_countable'
- Finset.measurableSet
- MeasureTheory.Integrable.of_finite
- integrableOn_Icc_iff_integrableOn_Ioo
- MeasureTheory.integrable_sum_dirac
- MeasureTheory.integrable_dirac
- ProbabilityTheory.HasLaw.ae_eq_of_dirac
- Measurable.factorsThrough
- MeasureTheory.integral_countable
- MeasureTheory.hasSum_integral_sum_dirac
- MeasureTheory.Measure.sum_smul_dirac
- Measurable.eq_const
- MeasurableSet.insert
- ProbabilityTheory.avgRisk_countable'
- MeasureTheory.lintegral_count
- PMF.toMeasure_apply_eq_toOuterMeasure
- integrableOn_Ioc_iff_integrableOn_Ioo
- MeasureTheory.aemeasurable_dirac
- ProbabilityTheory.map_cast_binomial_real_singleton
- MeasureTheory.integral_singleton
- Set.Subsingleton.measurableSet
- measurable_of_countable
- MeasureTheory.ae_eq_dirac'
- MeasureTheory.integral_sum_dirac
- MeasureTheory.restrict_dirac
- MeasureTheory.lintegral_fintype
- integrableOn_Icc_iff_integrableOn_Ioc'
Ancestors0
No ancestors.