'D' (Global Index)

Files

Definitions

Lemmas

Abbreviations

Global Index

D

dadd [prf, in mathcomp.analysis.derive]
dadd0e_subproof [prf, in mathcomp.reals.constructive_ereal]
dadde_snum [def, in mathcomp.reals.constructive_ereal]
dadde_snum_subproof [prf, in mathcomp.reals.constructive_ereal]
daddeA_subproof [prf, in mathcomp.reals.constructive_ereal]
daddeC_subproof [prf, 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]
davg.continuous_cvg_davg.continuous_davg_fin_num [var, in mathcomp.analysis.lebesgue_integral]
davg.continuous_cvg_davg.continuous_integralB_fin_num [var, in mathcomp.analysis.lebesgue_integral]
davg.continuous_cvg_davg.f [var, in mathcomp.analysis.lebesgue_integral]
davg.continuous_cvg_davg.fx [var, in mathcomp.analysis.lebesgue_integral]
davg.continuous_cvg_davg.mU [var, in mathcomp.analysis.lebesgue_integral]
davg.continuous_cvg_davg.mUf [var, in mathcomp.analysis.lebesgue_integral]
davg.continuous_cvg_davg.U [var, in mathcomp.analysis.lebesgue_integral]
davg.continuous_cvg_davg.x [var, in mathcomp.analysis.lebesgue_integral]
davg.continuous_cvg_davg.xU [var, in mathcomp.analysis.lebesgue_integral]
davg.R [var, in mathcomp.analysis.lebesgue_integral]
davg0 [prf, in mathcomp.analysis.lebesgue_integral]
davg_ge0 [prf, in mathcomp.analysis.lebesgue_integral]
davgD [prf, in mathcomp.analysis.lebesgue_integral]
dbilin [prf, in mathcomp.analysis.derive]
dcomp [prf, in mathcomp.analysis.derive]
dcst [prf, in mathcomp.analysis.derive]
dcvg [def, in mathcomp.experimental_reals.distr]
dcvg_homo [prf, in mathcomp.experimental_reals.distr]
dcvgP [prf, in mathcomp.experimental_reals.distr]
dec_segment_image [prf, in mathcomp.analysis.normedtype]
dec_surj_image_segment [prf, in mathcomp.analysis.normedtype]
dec_surj_image_segmentP [prf, in mathcomp.analysis.normedtype]
decide_or [prf, in mathcomp.classical.boolp]
decode [def, in mathcomp.reals.constructive_ereal]
decreasing_cvg_at_left_comp [prf, in mathcomp.analysis.ftc]
decreasing_cvg_at_right_comp [prf, in mathcomp.analysis.ftc]
decreasing_image_oo [prf, in mathcomp.analysis.ftc]
decreasing_opp [prf, in mathcomp.analysis.sequences]
decreasing_seqP [prf, in mathcomp.analysis.sequences]
default_measure_display [constr, in mathcomp.analysis.measure]
dEFin [def, in mathcomp.reals.constructive_ereal]
dEFin_snum [def, in mathcomp.reals.constructive_ereal]
dEFin_snum_subproof [prf, in mathcomp.reals.constructive_ereal]
deg_le2_ge0 [prf, in mathcomp.classical.mathcomp_extra]
dense [def, in mathcomp.analysis.topology_theory.topology_structure]
dense_rat [prf, in mathcomp.analysis.topology_theory.num_topology]
denseNE [prf, in mathcomp.analysis.topology_theory.topology_structure]
density.R [var, in mathcomp.analysis.lebesgue_integral]
dependent_choice_Type [prf, in mathcomp.classical.mathcomp_extra]
dependent_choice_Type.R [var, in mathcomp.classical.mathcomp_extra]
dependent_choice_Type.X [var, in mathcomp.classical.mathcomp_extra]
der_add [prf, in mathcomp.analysis.derive]
der_inv [prf, in mathcomp.analysis.derive]
der_mult [prf, in mathcomp.analysis.derive]
der_opp [prf, in mathcomp.analysis.derive]
der_scal [prf, in mathcomp.analysis.derive]
deriv1E [prf, in mathcomp.analysis.derive]
derivable [def, in mathcomp.analysis.derive]
derivable1_diffP [prf, in mathcomp.analysis.derive]
derivable1P [prf, in mathcomp.analysis.derive]
derivable_cos [prf, in mathcomp.analysis.trigo]
derivable_cst [prf, in mathcomp.analysis.derive]
derivable_expR [prf, in mathcomp.analysis.exp]
derivable_id [prf, in mathcomp.analysis.derive]
derivable_nbhs [prf, in mathcomp.analysis.derive]
derivable_nbhsP [prf, in mathcomp.analysis.derive]
derivable_nbhsx [prf, in mathcomp.analysis.derive]
derivable_nbhsxP [prf, in mathcomp.analysis.derive]
derivable_oo_continuous_bnd [def, in mathcomp.analysis.realfun]
derivable_oo_continuous_bnd.R [var, in mathcomp.analysis.realfun]
derivable_oo_continuous_bnd.V [var, in mathcomp.analysis.realfun]
derivable_oo_continuous_bnd_within [prf, in mathcomp.analysis.realfun]
derivable_sin [prf, in mathcomp.analysis.trigo]
derivable_sum [prf, in mathcomp.analysis.derive]
derivable_tan [prf, in mathcomp.analysis.trigo]
derivable_within_continuous [prf, in mathcomp.analysis.derive]
derivableB [prf, in mathcomp.analysis.derive]
derivableD [prf, in mathcomp.analysis.derive]
derivableM [prf, in mathcomp.analysis.derive]
derivableN [prf, in mathcomp.analysis.derive]
derivableP [prf, in mathcomp.analysis.derive]
derivableV [prf, in mathcomp.analysis.derive]
derivableX [prf, in mathcomp.analysis.derive]
derivableZ [prf, in mathcomp.analysis.derive]
derive [file, in mathcomp.analysis.derive]
derive [def, in mathcomp.analysis.derive]
derive1 [def, in mathcomp.analysis.derive]
derive1_at_max [prf, in mathcomp.analysis.derive]
derive1_at_min [prf, in mathcomp.analysis.derive]
derive1_atan [prf, in mathcomp.analysis.trigo]
derive1_comp [prf, in mathcomp.analysis.derive]
derive1_cst [prf, in mathcomp.analysis.derive]
derive1E [prf, in mathcomp.analysis.derive]
derive1E' [prf, in mathcomp.analysis.derive]
derive1n [def, in mathcomp.analysis.derive]
derive1n0 [prf, in mathcomp.analysis.derive]
derive1n1 [prf, in mathcomp.analysis.derive]
derive1nS [prf, in mathcomp.analysis.derive]
derive1Sn [prf, in mathcomp.analysis.derive]
derive_cst [prf, in mathcomp.analysis.derive]
derive_expR [prf, in mathcomp.analysis.exp]
derive_id [prf, in mathcomp.analysis.derive]
derive_id.R [var, in mathcomp.analysis.derive]
derive_id.V [var, in mathcomp.analysis.derive]
Derive_lemmasVR.R [var, in mathcomp.analysis.derive]
Derive_lemmasVR.V [var, in mathcomp.analysis.derive]
Derive_lemmasVW.R [var, in mathcomp.analysis.derive]
Derive_lemmasVW.V [var, in mathcomp.analysis.derive]
Derive_lemmasVW.W [var, in mathcomp.analysis.derive]
derive_sum [prf, in mathcomp.analysis.derive]
derive_val [proj, in mathcomp.analysis.derive]
deriveB [prf, in mathcomp.analysis.derive]
deriveD [prf, in mathcomp.analysis.derive]
deriveE [prf, in mathcomp.analysis.derive]
deriveM [prf, in mathcomp.analysis.derive]
deriveMl [prf, in mathcomp.analysis.derive]
deriveMr [prf, in mathcomp.analysis.derive]
derivemxE [prf, in mathcomp.analysis.derive]
deriveN [prf, in mathcomp.analysis.derive]
DeriveRU.der1 [var, in mathcomp.analysis.derive]
DeriveRU.R [var, in mathcomp.analysis.derive]
DeriveRU.U [var, in mathcomp.analysis.derive]
deriveV [prf, in mathcomp.analysis.derive]
DeriveVW.R [var, in mathcomp.analysis.derive]
DeriveVW.V [var, in mathcomp.analysis.derive]
DeriveVW.W [var, in mathcomp.analysis.derive]
deriveX [prf, in mathcomp.analysis.derive]
deriveZ [prf, in mathcomp.analysis.derive]
dflip [def, in mathcomp.experimental_reals.distr]
dflip1E [prf, in mathcomp.experimental_reals.distr]
dfst [abbrev, in mathcomp.experimental_reals.distr]
DFst.R [var, in mathcomp.experimental_reals.distr]
DFst.T [var, in mathcomp.experimental_reals.distr]
DFst.U [var, in mathcomp.experimental_reals.distr]
dfst_dswap [abbrev, in mathcomp.experimental_reals.distr]
dfstE [prf, in mathcomp.experimental_reals.distr]
DFunWith.f [var, in mathcomp.classical.mathcomp_extra]
DFunWith.I [var, in mathcomp.classical.mathcomp_extra]
DFunWith.T [var, in mathcomp.classical.mathcomp_extra]
DFunWithin [constr, in mathcomp.classical.mathcomp_extra]
DFunWithout [constr, in mathcomp.classical.mathcomp_extra]
dfwith [def, in mathcomp.classical.mathcomp_extra]
dfwith_continuous [prf, in mathcomp.analysis.function_spaces]
dfwith_spec [ind, in mathcomp.classical.mathcomp_extra]
dfwithin [prf, in mathcomp.classical.mathcomp_extra]
dfwithout [prf, in mathcomp.classical.mathcomp_extra]
dfwithP [prf, in mathcomp.classical.mathcomp_extra]
diagonal [def, in mathcomp.classical.classical_sets]
diagonalP [prf, in mathcomp.classical.classical_sets]
diff [def, in mathcomp.analysis.derive]
diff1E [prf, in mathcomp.analysis.derive]
diff_bilin [prf, in mathcomp.analysis.derive]
diff_comp [prf, in mathcomp.analysis.derive]
diff_continuous [prf, in mathcomp.analysis.derive]
diff_cst [prf, in mathcomp.analysis.derive]
diff_derivable [prf, in mathcomp.analysis.derive]
diff_eqO [prf, in mathcomp.analysis.derive]
diff_key [prf, in mathcomp.analysis.derive]
diff_lin [prf, in mathcomp.analysis.derive]
diff_locally [prf, in mathcomp.analysis.derive]
diff_locally_converse_part1 [prf, in mathcomp.analysis.derive]
diff_locallyP [prf, in mathcomp.analysis.derive]
diff_locallyx [prf, in mathcomp.analysis.derive]
diff_locallyxC [prf, in mathcomp.analysis.derive]
diff_locallyxP [prf, in mathcomp.analysis.derive]
diff_pair [prf, in mathcomp.analysis.derive]
diff_Rinv [prf, in mathcomp.analysis.derive]
diff_unique [prf, in mathcomp.analysis.derive]
diff_val [proj, in mathcomp.analysis.derive]
diffB [prf, in mathcomp.analysis.derive]
diffD [prf, in mathcomp.analysis.derive]
diffE [prf, in mathcomp.analysis.derive]
differentiable [abbrev, in mathcomp.analysis.derive]
differentiable [abbrev, in mathcomp.analysis.derive]
differentiable [abbrev, in mathcomp.analysis.derive]
differentiable_bilin [prf, in mathcomp.analysis.derive]
differentiable_comp [prf, in mathcomp.analysis.derive]
differentiable_continuous [prf, in mathcomp.analysis.derive]
differentiable_coord [prf, in mathcomp.analysis.derive]
differentiable_cst [prf, in mathcomp.analysis.derive]
differentiable_def [ind, in mathcomp.analysis.derive]
differentiable_pair [prf, in mathcomp.analysis.derive]
differentiable_Rinv [prf, in mathcomp.analysis.derive]
differentiable_sum [prf, in mathcomp.analysis.derive]
differentiableB [prf, in mathcomp.analysis.derive]
differentiableD [prf, in mathcomp.analysis.derive]
DifferentiableDef [constr, in mathcomp.analysis.derive]
differentiableM [prf, in mathcomp.analysis.derive]
differentiableN [prf, in mathcomp.analysis.derive]
differentiableP [prf, in mathcomp.analysis.derive]
differentiableV [prf, in mathcomp.analysis.derive]
differentiableX [prf, in mathcomp.analysis.derive]
differentiableZ [prf, in mathcomp.analysis.derive]
differentiableZl [prf, in mathcomp.analysis.derive]
'd [not, in mathcomp.analysis.derive] (no scope)
Differential.K [var, in mathcomp.analysis.derive]
Differential.V [var, in mathcomp.analysis.derive]
Differential.W [var, in mathcomp.analysis.derive]
'd [not, in mathcomp.analysis.derive] (no scope)
Differential_numFieldType.K [var, in mathcomp.analysis.derive]
Differential_numFieldType.V [var, in mathcomp.analysis.derive]
Differential_numFieldType.W [var, in mathcomp.analysis.derive]
'D_ [not, in mathcomp.analysis.derive] (no scope)
'D_ [not, in mathcomp.analysis.derive] (no scope)
DifferentialR.littleo_lemmas.X [var, in mathcomp.analysis.derive]
DifferentialR.littleo_lemmas.Y [var, in mathcomp.analysis.derive]
DifferentialR.littleo_lemmas.Z [var, in mathcomp.analysis.derive]
DifferentialR.R [var, in mathcomp.analysis.derive]
DifferentialR.V [var, in mathcomp.analysis.derive]
DifferentialR.W [var, in mathcomp.analysis.derive]
^` ( ) [not, in mathcomp.analysis.derive] (no scope)
^` () [not, in mathcomp.analysis.derive] (no scope)
DifferentialR2.R [var, in mathcomp.analysis.derive]
DifferentialR3.R [var, in mathcomp.analysis.derive]
DifferentialR3.V [var, in mathcomp.analysis.derive]
DifferentialR3.W [var, in mathcomp.analysis.derive]
DifferentialR3_numFieldType.R [var, in mathcomp.analysis.derive]
DifferentialR3_numFieldType.V [var, in mathcomp.analysis.derive]
DifferentialR3_numFieldType.W [var, in mathcomp.analysis.derive]
DifferentialR_numFieldType.R [var, in mathcomp.analysis.derive]
DifferentialR_numFieldType.V [var, in mathcomp.analysis.derive]
DifferentialR_numFieldType.W [var, in mathcomp.analysis.derive]
diffM [prf, in mathcomp.analysis.derive]
diffN [prf, in mathcomp.analysis.derive]
diffP [prf, in mathcomp.analysis.derive]
diffs_cos [prf, in mathcomp.analysis.trigo]
diffs_sin [prf, in mathcomp.analysis.trigo]
diffV [prf, in mathcomp.analysis.derive]
diffX [prf, in mathcomp.analysis.derive]
diffZ [prf, in mathcomp.analysis.derive]
diffZl [prf, in mathcomp.analysis.derive]
dinsupp [def, in mathcomp.experimental_reals.distr]
dinsupp_dlet [prf, in mathcomp.experimental_reals.distr]
dinsupp_restr [prf, in mathcomp.experimental_reals.distr]
dinsupp_swap [prf, in mathcomp.experimental_reals.distr]
dinsuppP [prf, in mathcomp.experimental_reals.distr]
dinsuppPn [prf, in mathcomp.experimental_reals.distr]
dinv [prf, in mathcomp.analysis.derive]
dirac [def, in mathcomp.analysis.measure]
dirac0 [prf, in mathcomp.analysis.measure]
dirac_lemmas.d [var, in mathcomp.analysis.measure]
dirac_lemmas.R [var, in mathcomp.analysis.measure]
dirac_lemmas.T [var, in mathcomp.analysis.measure]
dirac_lemmas_realFieldType.d [var, in mathcomp.analysis.measure]
dirac_lemmas_realFieldType.R [var, in mathcomp.analysis.measure]
dirac_lemmas_realFieldType.T [var, in mathcomp.analysis.measure]
dirac_measure.a [var, in mathcomp.analysis.measure]
dirac_measure.d [var, in mathcomp.analysis.measure]
dirac_measure.dirac0 [var, in mathcomp.analysis.measure]
dirac_measure.dirac_ge0 [var, in mathcomp.analysis.measure]
dirac_measure.dirac_sigma_additive [var, in mathcomp.analysis.measure]
dirac_measure.R [var, in mathcomp.analysis.measure]
dirac_measure.T [var, in mathcomp.analysis.measure]
diracE [prf, in mathcomp.analysis.measure]
diracT [prf, in mathcomp.analysis.measure]
discrete [file, in mathcomp.experimental_reals.discrete]
discrete_ball [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_ball_center [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_bool [prf, in mathcomp.analysis.topology_theory.bool_topology]
discrete_bool_compact [prf, in mathcomp.analysis.topology_theory.bool_topology]
discrete_closed [prf, in mathcomp.analysis.topology_theory.topology_structure]
discrete_cvg [prf, in mathcomp.analysis.topology_theory.topology_structure]
discrete_distribution.d [var, in mathcomp.analysis.probability]
discrete_distribution.P [var, in mathcomp.analysis.probability]
discrete_distribution.R [var, in mathcomp.analysis.probability]
discrete_distribution.T [var, in mathcomp.analysis.probability]
discrete_ent [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_hausdorff [prf, in mathcomp.analysis.separation_axioms]
discrete_measurable [def, in mathcomp.analysis.measure]
discrete_measurable.T [var, in mathcomp.analysis.measure]
discrete_measurable0 [prf, in mathcomp.analysis.measure]
discrete_measurableC [prf, in mathcomp.analysis.measure]
discrete_measurableU [prf, in mathcomp.analysis.measure]
discrete_nat [prf, in mathcomp.analysis.topology_theory.nat_topology]
discrete_nbhs [prf, in mathcomp.analysis.topology_theory.topology_structure]
discrete_open [prf, in mathcomp.analysis.topology_theory.topology_structure]
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.dsc [var, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_pseudoMetric.R [var, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_pseudoMetric.T [var, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_pseudometric_structure [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_random_variable [def, in mathcomp.analysis.probability]
discrete_set1 [prf, in mathcomp.analysis.topology_theory.topology_structure]
discrete_sing [prf, in mathcomp.analysis.topology_theory.topology_structure]
discrete_space [def, in mathcomp.analysis.topology_theory.topology_structure]
discrete_space_discrete [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_topology [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_topology.discrete_subproof [var, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_topology.hb_instance_39.P [var, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_topology.hb_instance_47.P [var, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_topology.hb_instance_53.P [var, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_topology.hb_instance_64.P [var, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_topology.hb_instance_73.P [var, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_topology.hb_instance_73.R [var, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_topology_type [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_uniform.dsc [var, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_uniform.T [var, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_uniform_structure [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_zero_dimension [prf, in mathcomp.analysis.separation_axioms]
discreteMeasurableFun [mod, in mathcomp.analysis.probability]
discreteMeasurableFun.axioms_ [rec, in mathcomp.analysis.probability]
discreteMeasurableFun.class [proj, in mathcomp.analysis.probability]
discreteMeasurableFun.Exports [mod, 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.lebesgue_integral_isMeasurableFun_mixin [proj, 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]
discreteMeasurableFun.probability_MeasurableFun_isDiscrete_mixin [proj, in mathcomp.analysis.probability]
discreteMeasurableFun.sort [proj, in mathcomp.analysis.probability]
discreteMeasurableFun.type [rec, in mathcomp.analysis.probability]
discreteMeasurableFunElpiOperations [mod, in mathcomp.analysis.probability]
DiscreteTopology.DiscreteMixin.X [var, in mathcomp.analysis.topology_theory.topology_structure]
DiscreteTopology.dsc [var, in mathcomp.analysis.topology_theory.topology_structure]
DiscreteTopology.X [var, in mathcomp.analysis.topology_theory.topology_structure]
disj_itv_Rhull [prf, in mathcomp.analysis.normedtype]
disj_set [def, in mathcomp.classical.classical_sets]
disj_set2E [prf, in mathcomp.classical.classical_sets]
disj_set2P [prf, in mathcomp.classical.classical_sets]
disj_set_some [prf, in mathcomp.classical.classical_sets]
disj_set_sym [prf, in mathcomp.classical.classical_sets]
disj_setPCl [prf, in mathcomp.classical.classical_sets]
disj_setPCr [prf, in mathcomp.classical.classical_sets]
disj_setPLR [prf, in mathcomp.classical.classical_sets]
disj_setPRL [prf, in mathcomp.classical.classical_sets]
disj_setPS [prf, in mathcomp.classical.classical_sets]
disjoint_caratheodoryIU [prf, in mathcomp.analysis.measure]
disjoint_itv [def, in mathcomp.classical.set_interval]
disjoint_itv.R [var, in mathcomp.classical.set_interval]
disjoint_itvxx [prf, in mathcomp.classical.set_interval]
disjoint_neitv [prf, in mathcomp.classical.set_interval]
disjoint_vitali_collection_partition [prf, in mathcomp.analysis.normedtype]
disjoints_subset [prf, in mathcomp.classical.classical_sets]
dist_sigma_algebra_instance.d [var, in mathcomp.analysis.measure]
dist_sigma_algebra_instance.R [var, in mathcomp.analysis.measure]
dist_sigma_algebra_instance.T [var, in mathcomp.analysis.measure]
distm_lt_split [prf, in mathcomp.analysis.normedtype]
distm_lt_splitl [prf, in mathcomp.analysis.normedtype]
distm_lt_splitr [prf, in mathcomp.analysis.normedtype]
distr [file, in mathcomp.experimental_reals.distr]
distr [abbrev, in mathcomp.experimental_reals.distr]
distr [abbrev, in mathcomp.experimental_reals.distr]
distr [rec, in mathcomp.experimental_reals.distr]
distr_of [def, in mathcomp.experimental_reals.distr]
DistrCoreTh.mu [var, in mathcomp.experimental_reals.distr]
DistrCoreTh.R [var, in mathcomp.experimental_reals.distr]
DistrCoreTh.T [var, in mathcomp.experimental_reals.distr]
DistrD.mu [var, in mathcomp.experimental_reals.distr]
DistrD.R [var, in mathcomp.experimental_reals.distr]
DistrD.T [var, in mathcomp.experimental_reals.distr]
distribution [def, in mathcomp.analysis.probability]
Distribution.R [var, in mathcomp.experimental_reals.distr]
Distribution.T [var, in mathcomp.experimental_reals.distr]
distribution_dRV [prf, in mathcomp.analysis.probability]
distribution_dRV.d [var, in mathcomp.analysis.probability]
distribution_dRV.d' [var, in mathcomp.analysis.probability]
distribution_dRV.measurable_set1T' [var, in mathcomp.analysis.probability]
distribution_dRV.P [var, in mathcomp.analysis.probability]
distribution_dRV.R [var, in mathcomp.analysis.probability]
distribution_dRV.T [var, in mathcomp.analysis.probability]
distribution_dRV.T' [var, in mathcomp.analysis.probability]
distribution_dRV.X [var, in mathcomp.analysis.probability]
distribution_dRV_enum [prf, in mathcomp.analysis.probability]
distribution_is_probability.d [var, in mathcomp.analysis.probability]
distribution_is_probability.d' [var, in mathcomp.analysis.probability]
distribution_is_probability.distribution0 [var, in mathcomp.analysis.probability]
distribution_is_probability.distribution_ge0 [var, in mathcomp.analysis.probability]
distribution_is_probability.distribution_is_probability [var, in mathcomp.analysis.probability]
distribution_is_probability.distribution_sigma_additive [var, in mathcomp.analysis.probability]
distribution_is_probability.P [var, in mathcomp.analysis.probability]
distribution_is_probability.R [var, in mathcomp.analysis.probability]
distribution_is_probability.T [var, in mathcomp.analysis.probability]
distribution_is_probability.T' [var, in mathcomp.analysis.probability]
distribution_is_probability.X [var, in mathcomp.analysis.probability]
DistrTheory.isd [var, in mathcomp.experimental_reals.distr]
DistrTheory.mu [var, in mathcomp.experimental_reals.distr]
DistrTheory.R [var, in mathcomp.experimental_reals.distr]
DistrTheory.T [var, in mathcomp.experimental_reals.distr]
diter [def, in mathcomp.experimental_reals.distr]
dlet [def, in mathcomp.experimental_reals.distr]
dlet_additive [prf, in mathcomp.experimental_reals.distr]
dlet_dinsupp [prf, in mathcomp.experimental_reals.distr]
dlet_dlet [abbrev, in mathcomp.experimental_reals.distr]
dlet_dmargin [abbrev, in mathcomp.experimental_reals.distr]
dlet_dunit_id [prf, in mathcomp.experimental_reals.distr]
dlet_eq0 [prf, in mathcomp.experimental_reals.distr]
dlet_lim [abbrev, in mathcomp.experimental_reals.distr]
dlet_null [prf, in mathcomp.experimental_reals.distr]
dlet_unit [prf, in mathcomp.experimental_reals.distr]
dletC [prf, in mathcomp.experimental_reals.distr]
dletE [prf, 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_let [abbrev, in mathcomp.experimental_reals.distr]
dlim_lift [def, in mathcomp.experimental_reals.distr]
dlim_spec [ind, in mathcomp.experimental_reals.distr]
dlim_ub [prf, in mathcomp.experimental_reals.distr]
dlimC [prf, in mathcomp.experimental_reals.distr]
DLimCvg [constr, in mathcomp.experimental_reals.distr]
dlimE [prf, in mathcomp.experimental_reals.distr]
DLimOut [constr, in mathcomp.experimental_reals.distr]
dlimP [prf, in mathcomp.experimental_reals.distr]
dlin [prf, in mathcomp.analysis.derive]
dmargin [def, in mathcomp.experimental_reals.distr]
dmargin_dlet [abbrev, in mathcomp.experimental_reals.distr]
dmargin_dunit [prf, in mathcomp.experimental_reals.distr]
dmargin_psumE [prf, in mathcomp.experimental_reals.distr]
dmarginE [prf, in mathcomp.experimental_reals.distr]
dnbhs [def, in mathcomp.analysis.topology_theory.topology_structure]
dnbhs0_le [prf, in mathcomp.analysis.normedtype]
dnbhs0_lt [prf, in mathcomp.analysis.normedtype]
dnbhs_ball [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
dnbhs_filter [inst, in mathcomp.analysis.topology_theory.topology_structure]
dnbhs_filter_on [def, in mathcomp.analysis.topology_theory.topology_structure]
dnbhsE [prf, in mathcomp.analysis.topology_theory.topology_structure]
dnbhsN [prf, in mathcomp.analysis.normedtype]
dnull [def, in mathcomp.experimental_reals.distr]
dnullE [prf, in mathcomp.experimental_reals.distr]
domain_change.d [var, in mathcomp.analysis.lebesgue_integral]
domain_change.mu [var, in mathcomp.analysis.lebesgue_integral]
domain_change.R [var, in mathcomp.analysis.lebesgue_integral]
domain_change.T [var, in mathcomp.analysis.lebesgue_integral]
dominated_by [def, in mathcomp.analysis.normedtype]
dominated_by1 [prf, in mathcomp.analysis.normedtype]
dominated_convergence [prf, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.absfg [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.cvg_g_ [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.D [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.d [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.f [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.f_ [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.f_f [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.fing [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.g [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.g0 [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.g_ [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.gg_ [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.gg_ge0 [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.ig [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.mD [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.mf [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.mf_ [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.mgg [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.mu [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.R [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_lemma.T [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.D [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.d [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.f [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.f_ [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.f_f [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.f_g [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.g [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.g_ [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.ig [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.mD [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.mf [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.mf_ [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.mu [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.R [var, in mathcomp.analysis.lebesgue_integral]
dominated_convergence_theorem.T [var, in mathcomp.analysis.lebesgue_integral]
dominated_cvg [prf, in mathcomp.analysis.lebesgue_integral]
dominated_cvg0 [prf, in mathcomp.analysis.lebesgue_integral]
dominated_integrable [prf, in mathcomp.analysis.lebesgue_integral]
dominates_cadd [prf, in mathcomp.analysis.charge]
dominates_charge_variation [prf, in mathcomp.analysis.charge]
dominates_cscalel [prf, in mathcomp.analysis.charge]
dominates_cscaler [prf, in mathcomp.analysis.charge]
dominates_induced [prf, in mathcomp.analysis.charge]
dominates_induced.d [var, in mathcomp.analysis.charge]
dominates_induced.f [var, in mathcomp.analysis.charge]
dominates_induced.intf [var, in mathcomp.analysis.charge]
dominates_induced.intnf [var, in mathcomp.analysis.charge]
dominates_induced.mu [var, in mathcomp.analysis.charge]
dominates_induced.R [var, in mathcomp.analysis.charge]
dominates_induced.T [var, in mathcomp.analysis.charge]
dominates_pushforward [prf, in mathcomp.analysis.charge]
dominates_uniform_prob [prf, in mathcomp.analysis.probability]
'a_o_ [not, in mathcomp.analysis.landau] (no scope)
'a_o_( \near ) [not, in mathcomp.analysis.landau] (no scope)
'o '_' [not, in mathcomp.analysis.landau] (no scope)
'o _( \near ) [not, in mathcomp.analysis.landau] (no scope)
'o_ [not, in mathcomp.analysis.landau] (no scope)
'o_( \near ) [not, in mathcomp.analysis.landau] (no scope)
[littleo of ] [not, in mathcomp.analysis.landau] (no scope)
[littleo of for ] [not, in mathcomp.analysis.landau] (no scope)
[o '_' of ] [not, in mathcomp.analysis.landau] (no scope)
[o _( \near ) of ] [not, in mathcomp.analysis.landau] (no scope)
[o_ of ] [not, in mathcomp.analysis.landau] (no scope)
[o_( \near ) of ] [not, in mathcomp.analysis.landau] (no scope)
{o_ } [not, in mathcomp.analysis.landau] (no scope)
= +o_ [not, in mathcomp.analysis.landau] (no scope)
= +o_( \near ) [not, in mathcomp.analysis.landau] (no scope)
== +o_ [not, in mathcomp.analysis.landau] (no scope)
== +o_( \near ) [not, in mathcomp.analysis.landau] (no scope)
==o_ [not, in mathcomp.analysis.landau] (no scope)
==o_( \near ) [not, in mathcomp.analysis.landau] (no scope)
=o_ [not, in mathcomp.analysis.landau] (no scope)
=o_( \near ) [not, in mathcomp.analysis.landau] (no scope)
Domination.hb_instance_1.F [var, in mathcomp.analysis.landau]
Domination.hb_instance_1.g [var, in mathcomp.analysis.landau]
Domination.K [var, in mathcomp.analysis.landau]
Domination.littleo_def [var, in mathcomp.analysis.landau]
Domination.T [var, in mathcomp.analysis.landau]
Domination.V [var, in mathcomp.analysis.landau]
Domination.W [var, in mathcomp.analysis.landau]
'a_O_ [not, in mathcomp.analysis.landau] (no scope)
'a_O_( \near ) [not, in mathcomp.analysis.landau] (no scope)
'O '_' [not, in mathcomp.analysis.landau] (no scope)
'O _( \near ) [not, in mathcomp.analysis.landau] (no scope)
'O_ [not, in mathcomp.analysis.landau] (no scope)
'O_( \near ) [not, in mathcomp.analysis.landau] (no scope)
[bigO of ] [not, in mathcomp.analysis.landau] (no scope)
[bigO of for ] [not, in mathcomp.analysis.landau] (no scope)
[o '_' of ] [not, in mathcomp.analysis.landau] (no scope)
[O '_' of ] [not, in mathcomp.analysis.landau] (no scope)
[O _( \near ) of ] [not, in mathcomp.analysis.landau] (no scope)
[o_ of ] [not, in mathcomp.analysis.landau] (no scope)
[O_ of ] [not, in mathcomp.analysis.landau] (no scope)
[O_( \near ) of ] [not, in mathcomp.analysis.landau] (no scope)
{o_ } [not, in mathcomp.analysis.landau] (no scope)
{O_ } [not, in mathcomp.analysis.landau] (no scope)
= +O_ [not, in mathcomp.analysis.landau] (no scope)
= +O_( \near ) [not, in mathcomp.analysis.landau] (no scope)
== +O_ [not, in mathcomp.analysis.landau] (no scope)
== +O_( \near ) [not, in mathcomp.analysis.landau] (no scope)
==O_ [not, in mathcomp.analysis.landau] (no scope)
==O_( \near ) [not, in mathcomp.analysis.landau] (no scope)
=O_ [not, in mathcomp.analysis.landau] (no scope)
=O_( \near ) [not, in mathcomp.analysis.landau] (no scope)
Domination_numFieldType.bigO_def [var, in mathcomp.analysis.landau]
Domination_numFieldType.bigO_ex_def [var, in mathcomp.analysis.landau]
Domination_numFieldType.hb_instance_4.F [var, in mathcomp.analysis.landau]
Domination_numFieldType.hb_instance_4.g [var, in mathcomp.analysis.landau]
Domination_numFieldType.K [var, in mathcomp.analysis.landau]
Domination_numFieldType.K [var, in mathcomp.analysis.landau]
Domination_numFieldType.littleo_def [var, in mathcomp.analysis.landau]
Domination_numFieldType.T [var, in mathcomp.analysis.landau]
Domination_numFieldType.T [var, in mathcomp.analysis.landau]
Domination_numFieldType.V [var, in mathcomp.analysis.landau]
Domination_numFieldType.V [var, in mathcomp.analysis.landau]
Domination_numFieldType.W [var, in mathcomp.analysis.landau]
Domination_numFieldType.W [var, in mathcomp.analysis.landau]
dopp [prf, in mathcomp.analysis.derive]
double_snum [def, in mathcomp.reals.signed]
double_snum_subproof [prf, in mathcomp.reals.signed]
down [def, in mathcomp.classical.classical_sets]
downK [prf, in mathcomp.reals.reals]
downP [prf, in mathcomp.classical.classical_sets]
dpair [prf, in mathcomp.analysis.derive]
drat [def, in mathcomp.experimental_reals.distr]
DRat.R [var, in mathcomp.experimental_reals.distr]
DRat.T [var, in mathcomp.experimental_reals.distr]
drat1E [prf, in mathcomp.experimental_reals.distr]
drestr [def, in mathcomp.experimental_reals.distr]
drestrD [prf, in mathcomp.experimental_reals.distr]
drestrE [prf, in mathcomp.experimental_reals.distr]
dRV_definitions.d [var, in mathcomp.analysis.probability]
dRV_definitions.d' [var, in mathcomp.analysis.probability]
dRV_definitions.P [var, in mathcomp.analysis.probability]
dRV_definitions.R [var, in mathcomp.analysis.probability]
dRV_definitions.T [var, in mathcomp.analysis.probability]
dRV_definitions.T' [var, in mathcomp.analysis.probability]
dRV_dom [def, in mathcomp.analysis.probability]
dRV_dom_enum [prf, in mathcomp.analysis.probability]
dRV_enum [def, in mathcomp.analysis.probability]
dRV_expectation [prf, in mathcomp.analysis.probability]
dscale [prf, in mathcomp.analysis.derive]
dscalel [prf, in mathcomp.analysis.derive]
dsnd [abbrev, in mathcomp.experimental_reals.distr]
DSnd.R [var, in mathcomp.experimental_reals.distr]
DSnd.T [var, in mathcomp.experimental_reals.distr]
DSnd.U [var, in mathcomp.experimental_reals.distr]
dsnd_dswap [abbrev, in mathcomp.experimental_reals.distr]
dsndE [abbrev, in mathcomp.experimental_reals.distr]
dswap [def, in mathcomp.experimental_reals.distr]
DSwap.A [var, in mathcomp.experimental_reals.distr]
DSwap.B [var, in mathcomp.experimental_reals.distr]
DSwap.mu [var, in mathcomp.experimental_reals.distr]
DSwap.R [var, in mathcomp.experimental_reals.distr]
DSwapCoreTheory.A [var, in mathcomp.experimental_reals.distr]
DSwapCoreTheory.B [var, in mathcomp.experimental_reals.distr]
DSwapCoreTheory.mu [var, in mathcomp.experimental_reals.distr]
DSwapCoreTheory.R [var, in mathcomp.experimental_reals.distr]
dswapE [prf, in mathcomp.experimental_reals.distr]
dswapK [prf, in mathcomp.experimental_reals.distr]
DSwapTheory.A [var, in mathcomp.experimental_reals.distr]
DSwapTheory.B [var, in mathcomp.experimental_reals.distr]
DSwapTheory.mu [var, in mathcomp.experimental_reals.distr]
DSwapTheory.R [var, in mathcomp.experimental_reals.distr]
dual_adde [def, in mathcomp.reals.constructive_ereal]
dual_extended [def, in mathcomp.reals.constructive_ereal]
DualAddTheory [mod, in mathcomp.reals.constructive_ereal]
DualAddTheory [mod, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain [mod, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain [mod, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.constructive_ereal_dEFin__canonical__GRing_Additive [def, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadd0e [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde_eq_pinfty [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde_ge0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde_le0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde_Neq_ninfty [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde_Neq_pinfty [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dadde_ss_eq0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeA [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeAC [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeACA [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeC [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeCA [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeK [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddeNy [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddey [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddNye [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.daddye [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dEFin_semi_additive [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dEFinB [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dEFinD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dEFinE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.desum_eqNy [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.desum_eqNyP [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.desum_eqy [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.desum_eqyP [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dfin_numD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dfineB [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dfineD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dfsume_ge0 [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.dfsume_gt0 [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.dfsume_le0 [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.dfsume_lt0 [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.dmule2n [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.doppeB [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.doppeD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsub0e [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsube0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsube_eq [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsubee [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsubeK [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsume_ge0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsume_le0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dsumEFin [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dual_addeE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dual_addeE_def [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.dual_fsumeE [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.dual_sumeE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.DualERealArithTh_numDomainType.R [var, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.DualERealArithTh_numDomainType.R [var, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.DualERealArithTh_realDomainType.R [var, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.ednatmul_ninfty [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.ednatmul_pinfty [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.ednatmulE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.EFin_dnatmul [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.fin_num_doppeB [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.fin_num_doppeD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.finite_supportNe [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.gte_dN [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.gte_dopp [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.HB_unnamed_factory_40 [def, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.le0_mule_dfsuml [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.le0_mule_dfsumr [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.ndadde_eq0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.pdadde_eq0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.pdfsume_eq0 [prf, in mathcomp.analysis.ereal]
DualAddTheoryNumDomain.realDed [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryNumDomain.sqredD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain [mod, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dadde_minl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dadde_minr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dge0_muleDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dge0_muleDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dle0_muleDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dle0_muleDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dmule_natl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dmuleDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dmuleDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsube_ge0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsube_gt0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsube_le0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsube_lt0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsuber_gt0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsuber_le0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsubre_gt0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.dsubre_le0 [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.DualERealArithTh_realDomainType.R [var, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.ge0_dsume_distrl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.ge0_dsume_distrr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gee_daddl [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gee_daddr [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gee_dDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gee_dDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gte_daddl [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gte_daddr [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gte_dBl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gte_dBr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gte_dDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gte_dDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gte_dsubl [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gte_dsubr [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.le0_dsume_distrl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.le0_dsume_distrr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_abs_dadd [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_abs_dsub [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_abs_dsum [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dadd [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dadd2l [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dadd2r [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dadd2rE [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_daddl [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_daddr [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dB [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dD2l [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dD2lE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dD2r [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dD2rE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsub [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsubel_addl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsubel_addr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsuber_addl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsuber_addr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsubl_addl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsubl_addr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsubr_addl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsubr_addr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_nneg [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_nneg_natl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_nneg_natr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_nneg_ord [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_nneg_subfset [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_nneg_subset [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_npos [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_npos_natl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_npos_natr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_npos_ord [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_npos_subfset [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_dsum_npos_subset [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_lt_dadd [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_lt_dD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_pdaddl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_pdaddr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dadd [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dadd2lE [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_daddl [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_daddr [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dBlDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dBlDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dBrDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dBrDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dD2lE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dD2rE [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dDr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dsubel_addl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dsubel_addr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dsuber_addl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dsuber_addr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dsubl_addl [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dsubl_addr [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dsubr_addl [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_dsubr_addr [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_le_dadd [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_le_dB [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_le_dD [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_le_dsub [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_pdaddl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_pdaddr [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_spdadder [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_spdaddre [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealField [mod, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealField.DualRealFieldType_lemmas.R [var, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealField.lee_daddgt0Pr [prf, in mathcomp.reals.constructive_ereal]
ducvg [def, in mathcomp.experimental_reals.distr]
duni [def, in mathcomp.experimental_reals.distr]
duni1E [prf, in mathcomp.experimental_reals.distr]
dunit [def, in mathcomp.experimental_reals.distr]
dunit1E [prf, in mathcomp.experimental_reals.distr]
dvg_approx [prf, in mathcomp.analysis.lebesgue_integral]
dvg_ereal_cvg [abbrev, in mathcomp.analysis.sequences]
dvg_harmonic [prf, in mathcomp.analysis.sequences]
dvg_inP [prf, in mathcomp.classical.filter]
dvg_nseries [prf, in mathcomp.analysis.sequences]
dvg_riemannR [prf, in mathcomp.analysis.exp]
dvgP [prf, in mathcomp.classical.filter]
dweight [abbrev, in mathcomp.experimental_reals.distr]
dyadic_approx [def, in mathcomp.analysis.lebesgue_integral]
dyadic_interval.R [var, in mathcomp.analysis.lebesgue_integral]
dyadic_itv [def, in mathcomp.analysis.lebesgue_integral]
dyadic_itv_image [prf, in mathcomp.analysis.lebesgue_integral]
dyadic_itv_subU [prf, in mathcomp.analysis.lebesgue_integral]
dynkin [def, in mathcomp.analysis.measure]
dynkin.T [var, in mathcomp.analysis.measure]
dynkin_g_dynkin [abbrev, in mathcomp.analysis.measure]
dynkin_lambda_system [prf, in mathcomp.analysis.measure]
dynkin_lemmas.T [var, in mathcomp.analysis.measure]
dynkin_monotone [abbrev, in mathcomp.analysis.measure]
dynkin_setI_sigma_algebra [prf, in mathcomp.analysis.measure]
dynkinC [prf, in mathcomp.analysis.measure]
dynkinT [prf, in mathcomp.analysis.measure]
dynkinU [prf, in mathcomp.analysis.measure]