'D' (Definitions)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | * |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | * |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | * |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | * |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | * |
D (Definitions)
dadde_snum [def, in mathcomp.reals.constructive_ereal]Datatypes_bool__canonical__classical_sets_Pointed [def, in mathcomp.classical.classical_sets]
Datatypes_bool__canonical__filter_Filtered [def, in mathcomp.classical.filter]
Datatypes_bool__canonical__filter_Nbhs [def, in mathcomp.classical.filter]
Datatypes_bool__canonical__filter_PointedFiltered [def, in mathcomp.classical.filter]
Datatypes_bool__canonical__filter_PointedNbhs [def, in mathcomp.classical.filter]
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_bool__canonical__measure_SigmaRing [def, in mathcomp.analysis.measure]
Datatypes_bool__canonical__order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__topology_structure_PointedTopological [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_Empty_set__canonical__classical_sets_Empty [def, in mathcomp.classical.classical_sets]
Datatypes_nat__canonical__classical_sets_Pointed [def, in mathcomp.classical.classical_sets]
Datatypes_nat__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__filter_PointedFiltered [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__filter_PointedNbhs [def, in mathcomp.analysis.topology_theory.nat_topology]
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_nat__canonical__measure_SigmaRing [def, in mathcomp.analysis.measure]
Datatypes_nat__canonical__order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__topology_structure_PointedTopological [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_option__canonical__classical_sets_Pointed [def, in mathcomp.classical.classical_sets]
Datatypes_prod__canonical__classical_sets_Pointed [def, in mathcomp.classical.classical_sets]
Datatypes_prod__canonical__filter_Filtered [def, in mathcomp.classical.filter]
Datatypes_prod__canonical__filter_Nbhs [def, in mathcomp.classical.filter]
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_prod__canonical__measure_SigmaRing [def, in mathcomp.analysis.measure]
Datatypes_prod__canonical__normedtype_NormedModule [def, in mathcomp.analysis.normedtype]
Datatypes_prod__canonical__normedtype_PseudoMetricNormedZmod [def, in mathcomp.analysis.normedtype]
Datatypes_prod__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.product_topology]
Datatypes_prod__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.product_topology]
Datatypes_prod__canonical__tvs_Tvs [def, in mathcomp.analysis.tvs]
Datatypes_prod__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.product_topology]
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__classical_sets_Pointed [def, in mathcomp.classical.classical_sets]
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]
Datatypes_unit__canonical__measure_SigmaRing [def, in mathcomp.analysis.measure]
davg [def, in mathcomp.analysis.lebesgue_integral]
dcvg [def, in mathcomp.experimental_reals.distr]
decode [def, in mathcomp.reals.constructive_ereal]
dEFin [def, in mathcomp.reals.constructive_ereal]
dEFin_snum [def, in mathcomp.reals.constructive_ereal]
dense [def, in mathcomp.analysis.topology_theory.topology_structure]
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]
dflip [def, in mathcomp.experimental_reals.distr]
dfwith [def, in mathcomp.classical.mathcomp_extra]
diagonal [def, in mathcomp.classical.classical_sets]
diff [def, in mathcomp.analysis.derive]
dinsupp [def, in mathcomp.experimental_reals.distr]
dirac [def, in mathcomp.analysis.measure]
discrete_ball [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_ent [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_measurable [def, in mathcomp.analysis.measure]
discrete_pred_sub__canonical__choice_Choice [def, in mathcomp.experimental_reals.discrete]
discrete_pred_sub__canonical__choice_Countable [def, in mathcomp.experimental_reals.discrete]
discrete_pred_sub__canonical__choice_SubChoice [def, in mathcomp.experimental_reals.discrete]
discrete_pred_sub__canonical__choice_SubCountable [def, in mathcomp.experimental_reals.discrete]
discrete_pred_sub__canonical__eqtype_Equality [def, in mathcomp.experimental_reals.discrete]
discrete_pred_sub__canonical__eqtype_SubEquality [def, in mathcomp.experimental_reals.discrete]
discrete_pred_sub__canonical__eqtype_SubType [def, in mathcomp.experimental_reals.discrete]
discrete_pseudometric_structure [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_random_variable [def, in mathcomp.analysis.probability]
discrete_space [def, in mathcomp.analysis.topology_theory.topology_structure]
discrete_topology [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_topology_type [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_uniform_structure [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
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]
distr_of [def, in mathcomp.experimental_reals.distr]
distribution [def, in mathcomp.analysis.probability]
diter [def, in mathcomp.experimental_reals.distr]
dlet [def, in mathcomp.experimental_reals.distr]
dlift [def, in mathcomp.experimental_reals.distr]
dlim [def, in mathcomp.experimental_reals.distr]
dlim_bump [def, in mathcomp.experimental_reals.distr]
dlim_lift [def, in mathcomp.experimental_reals.distr]
dmargin [def, in mathcomp.experimental_reals.distr]
dnbhs [def, in mathcomp.analysis.topology_theory.topology_structure]
dnbhs_filter_on [def, in mathcomp.analysis.topology_theory.topology_structure]
dnull [def, in mathcomp.experimental_reals.distr]
dominated_by [def, in mathcomp.analysis.normedtype]
double_snum [def, in mathcomp.reals.signed]
down [def, in mathcomp.classical.classical_sets]
drat [def, in mathcomp.experimental_reals.distr]
drestr [def, in mathcomp.experimental_reals.distr]
dRV_dom [def, in mathcomp.analysis.probability]
dRV_enum [def, in mathcomp.analysis.probability]
dswap [def, in mathcomp.experimental_reals.distr]
dual_adde [def, in mathcomp.reals.constructive_ereal]
dual_extended [def, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.constructive_ereal_dEFin__canonical__GRing_Additive [def, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.HB_unnamed_factory_40 [def, in mathcomp.reals.constructive_ereal]
ducvg [def, in mathcomp.experimental_reals.distr]
duni [def, in mathcomp.experimental_reals.distr]
dunit [def, in mathcomp.experimental_reals.distr]
dyadic_approx [def, in mathcomp.analysis.lebesgue_integral]
dyadic_itv [def, in mathcomp.analysis.lebesgue_integral]
dynkin [def, in mathcomp.analysis.measure]