D (Definitions)
dadde_snum [def, in mathcomp.analysis.constructive_ereal]
Datatypes_bool__canonical__measure_AlgebraOfSets [def, in mathcomp.analysis.measure]
Datatypes_bool__canonical__measure_Measurable [def, in mathcomp.analysis.measure]
Datatypes_bool__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
Datatypes_bool__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
Datatypes_nat__canonical__measure_AlgebraOfSets [def, in mathcomp.analysis.measure]
Datatypes_nat__canonical__measure_Measurable [def, in mathcomp.analysis.measure]
Datatypes_nat__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
Datatypes_nat__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
Datatypes_prod__canonical__measure_AlgebraOfSets [def, in mathcomp.analysis.measure]
Datatypes_prod__canonical__measure_Measurable [def, in mathcomp.analysis.measure]
Datatypes_prod__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
Datatypes_prod__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
Datatypes_Some__canonical__functions_Bij [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_Fun [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_Inject [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_Surject [def, in mathcomp.classical.functions]
Datatypes_Some__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Datatypes_unit__canonical__measure_AlgebraOfSets [def, in mathcomp.analysis.measure]
Datatypes_unit__canonical__measure_Measurable [def, in mathcomp.analysis.measure]
Datatypes_unit__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
Datatypes_unit__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
decode [def, in mathcomp.analysis.constructive_ereal]
Def_normr__canonical__lebesgue_integral_MeasurableFun [def, in mathcomp.analysis.lebesgue_integral]
dense [def, in mathcomp.analysis.topology]
dep_arrow_choiceClass [def, in mathcomp.classical.boolp]
dep_arrow_choiceType [def, in mathcomp.classical.boolp]
dep_arrow_eqType [def, in mathcomp.classical.boolp]
dep_arrow_pointedType [def, in mathcomp.classical.classical_sets]
derivable [def, in mathcomp.analysis.derive]
derivable_oo_continuous_bnd [def, in mathcomp.analysis.realfun]
derive [def, in mathcomp.analysis.derive]
derive1 [def, in mathcomp.analysis.derive]
derive1n [def, in mathcomp.analysis.derive]
dfwith [def, in mathcomp.classical.mathcomp_extra]
diff [def, in mathcomp.analysis.derive]
dirac [def, in mathcomp.analysis.measure]
discrete_ball [def, in mathcomp.analysis.topology]
discrete_ent [def, in mathcomp.analysis.topology]
discrete_measurable_bool [def, in mathcomp.analysis.measure]
discrete_measurable_nat [def, in mathcomp.analysis.measure]
discrete_measurable_unit [def, in mathcomp.analysis.measure]
discrete_pseudoMetricType [def, in mathcomp.analysis.topology]
discrete_pseudoMetricType_mixin [def, in mathcomp.analysis.topology]
discrete_random_variable [def, in mathcomp.analysis.probability]
discrete_space [def, in mathcomp.analysis.topology]
discrete_topological_mixin [def, in mathcomp.analysis.topology]
discrete_uniform_mixin [def, in mathcomp.analysis.topology]
discrete_uniformType [def, in mathcomp.analysis.topology]
discreteMeasurableFun.EtaAndMixinExports.HB_unnamed_factory_18 [def, in mathcomp.analysis.probability]
discreteMeasurableFun.EtaAndMixinExports.HB_unnamed_mixin_21 [def, in mathcomp.analysis.probability]
discreteMeasurableFun.EtaAndMixinExports.probability_discreteMeasurableFun__to__lebesgue_integral_isMeasurableFun [def, in mathcomp.analysis.probability]
discreteMeasurableFun.EtaAndMixinExports.probability_discreteMeasurableFun__to__probability_MeasurableFun_isDiscrete [def, in mathcomp.analysis.probability]
discreteMeasurableFun.EtaAndMixinExports.structures_eta__canonical__probability_discreteMeasurableFun [def, in mathcomp.analysis.probability]
discreteMeasurableFun.Exports.probability_discreteMeasurableFun__to__lebesgue_integral_MeasurableFun [def, in mathcomp.analysis.probability]
discreteMeasurableFun.Exports.probability_discreteMeasurableFun_class__to__lebesgue_integral_MeasurableFun_class [def, in mathcomp.analysis.probability]
discreteMeasurableFun.pack_ [def, in mathcomp.analysis.probability]
discreteMeasurableFun.phant_clone [def, in mathcomp.analysis.probability]
discreteMeasurableFun.phant_on_ [def, in mathcomp.analysis.probability]
disj_set [def, in mathcomp.classical.classical_sets]
disjoint_itv [def, in mathcomp.classical.set_interval]
distN [def, in mathcomp.analysis.topology]
distribution [def, in mathcomp.analysis.probability]
dnbhs [def, in mathcomp.analysis.topology]
dnbhs_filter_on [def, in mathcomp.analysis.topology]
dominated_by [def, in mathcomp.analysis.normedtype]
double_snum [def, in mathcomp.analysis.signed]
down [def, in mathcomp.classical.classical_sets]
dRV_dom [def, in mathcomp.analysis.probability]
dRV_dom_enum [def, in mathcomp.analysis.probability]
dRV_enum [def, in mathcomp.analysis.probability]
dual_adde [def, in mathcomp.analysis.constructive_ereal]
dual_adde_subdef [def, in mathcomp.analysis.constructive_ereal]
dual_extended [def, in mathcomp.analysis.constructive_ereal]
DualAddTheoryNumDomain.dadde_comoid [def, in mathcomp.analysis.constructive_ereal]
DualAddTheoryNumDomain.dadde_monoid [def, in mathcomp.analysis.constructive_ereal]
dyadic_itv [def, in mathcomp.analysis.lebesgue_integral]
dynkin [def, in mathcomp.analysis.measure]