'D' (Global Index)

Files

J

V

Y

Z

_

*

Definitions

_

*

Lemmas

*

Abbreviations

J

K

Y

Z

_

*

Global Index

D

dadd [prf, in mathcomp.analysis.derive]
dadde_snum [def, in mathcomp.reals.constructive_ereal]
Datatypes_bool__canonical__classical_sets_Pointed [def, in mathcomp.classical.classical_sets]
Datatypes_bool__canonical__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__discrete_topology_DiscreteOrderTopology [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__discrete_topology_DiscretePseudoMetric [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__discrete_topology_DiscreteUniform [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__discrete_topology_PointedDiscreteOrderTopology [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__discrete_topology_PointedDiscreteTopology [def, in mathcomp.analysis.topology_theory.bool_topology]
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_OrderPseudoMetric [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__order_topology_OrderUniform [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__pseudometric_structure_PseudoPointedMetric [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_bool__canonical__uniform_structure_PointedUniform [def, in mathcomp.analysis.topology_theory.bool_topology]
Datatypes_bool__canonical__uniform_structure_Uniform [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__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__discrete_topology_DiscreteOrderTopology [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__discrete_topology_DiscretePseudoMetric [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__discrete_topology_DiscreteUniform [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__discrete_topology_PointedDiscreteOrderTopology [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__discrete_topology_PointedDiscreteTopology [def, in mathcomp.analysis.topology_theory.nat_topology]
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_OrderPseudoMetric [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__order_topology_OrderUniform [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__pseudometric_structure_PseudoPointedMetric [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_nat__canonical__uniform_structure_PointedUniform [def, in mathcomp.analysis.topology_theory.nat_topology]
Datatypes_nat__canonical__uniform_structure_Uniform [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]
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]
decr_derive1_le0 [prf, in mathcomp.analysis.derive]
decr_derive1_le0_itv [prf, in mathcomp.analysis.derive]
decr_derive1_le0_itvNy [prf, in mathcomp.analysis.derive]
decr_derive1_le0_itvy [prf, in mathcomp.analysis.derive]
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]
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]
dependent_choice_Type [prf, 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_atan [prf, in mathcomp.analysis.trigo]
derivable_cos [prf, in mathcomp.analysis.trigo]
derivable_cst [prf, in mathcomp.analysis.derive]
derivable_expR [prf, in mathcomp.analysis.exp]
derivable_horner [prf, in mathcomp.analysis.derive]
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_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_under_integral [prf, in mathcomp.analysis.ftc]
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 [prf, 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_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]
deriveV [prf, 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_dswap [abbrev, in mathcomp.experimental_reals.distr]
dfstE [prf, in mathcomp.experimental_reals.distr]
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)
'd [not, in mathcomp.analysis.derive] (no scope)
'D_ [not, in mathcomp.analysis.derive] (no scope)
'D_ [not, in mathcomp.analysis.derive] (no scope)
^` ( ) [not, in mathcomp.analysis.derive] (no scope)
^` () [not, in mathcomp.analysis.derive] (no scope)
differentiation_under_integral [prf, in mathcomp.analysis.ftc]
'd1 [not, in mathcomp.analysis.ftc] (no scope)
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]
diracE [prf, in mathcomp.analysis.measure]
diracT [prf, in mathcomp.analysis.measure]
discontinuity [def, in mathcomp.analysis.realfun]
discontinuity_countable [prf, in mathcomp.analysis.realfun]
discrete [file, in mathcomp.experimental_reals.discrete]
discrete_ball [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_closed [prf, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_cvg [prf, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_ent [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_hausdorff [prf, in mathcomp.analysis.separation_axioms]
discrete_measurable [def, 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_ofNbhs [mod, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.axioms_ [rec, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.Discrete_ofNbhs_T__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.Discrete_ofNbhs_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.Discrete_ofNbhs_T__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.Discrete_ofNbhs_T__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.Exports [mod, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.identity_builder [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.nbhs_principalE [proj, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric [mod, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.axioms_ [rec, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Discrete_ofPseudometric_T__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Exports [mod, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.identity_builder [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.metric_discrete [proj, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform [mod, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.axioms_ [rec, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Discrete_ofUniform_T__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Discrete_ofUniform_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Discrete_ofUniform_T__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Discrete_ofUniform_T__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Discrete_ofUniform_T__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Discrete_ofUniform_T__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Exports [mod, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.identity_builder [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.uniform_discrete [proj, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_open [prf, in mathcomp.analysis.topology_theory.discrete_topology]
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_random_variable [def, in mathcomp.analysis.probability]
discrete_set1 [prf, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology [file, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_Discrete_ofNbhs__to__topology_structure_Nbhs_isTopological [def, in mathcomp.analysis.topology_theory.nat_topology]
discrete_topology_Discrete_ofNbhs__to__topology_structure_Nbhs_isTopological [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_Discrete_ofNbhs__to__topology_structure_Nbhs_isTopological [def, in mathcomp.analysis.topology_theory.bool_topology]
discrete_topology_discrete_topology__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__classical_sets_Pointed [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__discrete_topology_DiscretePseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__discrete_topology_DiscreteUniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_discrete_topology__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_DiscretePseudoMetric_ofUniform__to__discrete_topology_Discrete_ofPseudometric [def, in mathcomp.analysis.topology_theory.nat_topology]
discrete_topology_DiscretePseudoMetric_ofUniform__to__discrete_topology_Discrete_ofPseudometric [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_DiscretePseudoMetric_ofUniform__to__discrete_topology_Discrete_ofPseudometric [def, in mathcomp.analysis.topology_theory.bool_topology]
discrete_topology_DiscretePseudoMetric_ofUniform__to__pseudometric_structure_Uniform_isPseudoMetric [def, in mathcomp.analysis.topology_theory.nat_topology]
discrete_topology_DiscretePseudoMetric_ofUniform__to__pseudometric_structure_Uniform_isPseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_DiscretePseudoMetric_ofUniform__to__pseudometric_structure_Uniform_isPseudoMetric [def, in mathcomp.analysis.topology_theory.bool_topology]
discrete_topology_DiscreteTopology__to__choice_hasChoice [def, in mathcomp.analysis.cantor]
discrete_topology_DiscreteTopology__to__discrete_topology_Discrete_ofNbhs [def, in mathcomp.analysis.cantor]
discrete_topology_DiscreteTopology__to__eqtype_hasDecEq [def, in mathcomp.analysis.cantor]
discrete_topology_DiscreteTopology__to__filter_isFiltered [def, in mathcomp.analysis.cantor]
discrete_topology_DiscreteTopology__to__filter_selfFiltered [def, in mathcomp.analysis.cantor]
discrete_topology_DiscreteTopology__to__topology_structure_Nbhs_isTopological [def, in mathcomp.analysis.cantor]
discrete_topology_DiscreteUniform_ofNbhs__to__discrete_topology_Discrete_ofUniform [def, in mathcomp.analysis.topology_theory.nat_topology]
discrete_topology_DiscreteUniform_ofNbhs__to__discrete_topology_Discrete_ofUniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_DiscreteUniform_ofNbhs__to__discrete_topology_Discrete_ofUniform [def, in mathcomp.analysis.topology_theory.bool_topology]
discrete_topology_DiscreteUniform_ofNbhs__to__uniform_structure_Nbhs_isUniform_mixin [def, in mathcomp.analysis.topology_theory.nat_topology]
discrete_topology_DiscreteUniform_ofNbhs__to__uniform_structure_Nbhs_isUniform_mixin [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_topology_DiscreteUniform_ofNbhs__to__uniform_structure_Nbhs_isUniform_mixin [def, in mathcomp.analysis.topology_theory.bool_topology]
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]
DiscreteNbhs [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.axioms_ [rec, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.choice_hasChoice_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.class [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.discrete_topology_Discrete_ofNbhs_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs__to__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discrete_topology_DiscreteNbhs_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.filter_isFiltered_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.filter_selfFiltered_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.sort [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.type [rec, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhsElpiOperations [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.axioms_ [rec, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.choice_hasChoice_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.class [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.discrete_topology_Discrete_ofNbhs_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__Order_DistrLattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__Order_JoinSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__Order_Lattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__Order_MeetSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__Order_POrder [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__Order_Total [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology__to__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__discrete_topology_DiscreteNbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__discrete_topology_DiscreteTopology_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__Order_DistrLattice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__Order_JoinSemilattice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__Order_Lattice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__Order_MeetSemilattice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__Order_POrder_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__order_topology_OrderNbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__order_topology_OrderTopological_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__Order_Total_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discrete_topology_DiscreteOrderTopology_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_DistrLattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_JoinSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_Lattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_MeetSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_POrder [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteNbhs_and_Order_Total [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_DistrLattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_JoinSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_Lattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_MeetSemilattice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_POrder [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_order_topology_OrderNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_order_topology_OrderTopological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.join_discrete_topology_DiscreteOrderTopology_between_discrete_topology_DiscreteTopology_and_Order_Total [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.filter_isFiltered_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.filter_selfFiltered_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Order_DistrLattice_isTotal_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Order_isDuallyPOrder_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Order_Lattice_isDistributive_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Order_POrder_isJoinSemilattice_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Order_POrder_isMeetSemilattice_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.order_topology_Order_isNbhs_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.sort [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.type [rec, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopologyElpiOperations [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.axioms_ [rec, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.choice_hasChoice_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.class [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.discrete_topology_Discrete_ofNbhs_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.discrete_topology_Discrete_ofPseudometric_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.discrete_topology_Discrete_ofUniform_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__discrete_topology_DiscreteUniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric__to__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__discrete_topology_DiscreteNbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__discrete_topology_DiscreteTopology_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__discrete_topology_DiscreteUniform_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__pseudometric_structure_PseudoMetric_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discrete_topology_DiscretePseudoMetric_class__to__uniform_structure_Uniform_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.join_discrete_topology_DiscretePseudoMetric_between_discrete_topology_DiscreteNbhs_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.join_discrete_topology_DiscretePseudoMetric_between_discrete_topology_DiscreteTopology_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.join_discrete_topology_DiscretePseudoMetric_between_discrete_topology_DiscreteUniform_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.filter_isFiltered_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.filter_selfFiltered_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.pseudometric_structure_Uniform_isPseudoMetric_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.sort [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.type [rec, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.uniform_structure_Nbhs_isUniform_mixin_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.axioms_ [rec, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__discrete_topology_DiscreteUniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.DiscretePseudoMetric_ofUniform_T__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.Exports [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetricElpiOperations [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.axioms_ [rec, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.choice_hasChoice_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.class [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.discrete_topology_Discrete_ofNbhs_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology__to__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology__to__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology__to__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology_class__to__discrete_topology_DiscreteNbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discrete_topology_DiscreteTopology_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.join_discrete_topology_DiscreteTopology_between_discrete_topology_DiscreteNbhs_and_topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.filter_isFiltered_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.filter_selfFiltered_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.sort [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.type [rec, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopologyElpiOperations [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.axioms_ [rec, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.choice_hasChoice_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.class [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.discrete_topology_Discrete_ofNbhs_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.discrete_topology_Discrete_ofUniform_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform__to__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__discrete_topology_DiscreteNbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__discrete_topology_DiscreteTopology_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discrete_topology_DiscreteUniform_class__to__uniform_structure_Uniform_class [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.join_discrete_topology_DiscreteUniform_between_discrete_topology_DiscreteNbhs_and_uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.join_discrete_topology_DiscreteUniform_between_discrete_topology_DiscreteTopology_and_uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.filter_isFiltered_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.filter_selfFiltered_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.pack_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.phant_clone [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.phant_on_ [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.sort [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.type [rec, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.uniform_structure_Nbhs_isUniform_mixin_mixin [proj, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.axioms_ [rec, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__discrete_topology_DiscreteNbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__discrete_topology_DiscreteTopology [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.DiscreteUniform_ofNbhs_T__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.Exports [mod, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniformElpiOperations [mod, in mathcomp.analysis.topology_theory.discrete_topology]
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_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]
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]
distribution [def, in mathcomp.analysis.probability]
distribution_dRV [prf, in mathcomp.analysis.probability]
distribution_dRV_enum [prf, in mathcomp.analysis.probability]
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]
dominated_by [def, in mathcomp.analysis.normedtype]
dominated_by1 [prf, in mathcomp.analysis.normedtype]
dominated_convergence [prf, 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_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)
'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)
dopp [prf, in mathcomp.analysis.derive]
double_snum [def, 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]
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_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_dswap [abbrev, in mathcomp.experimental_reals.distr]
dsndE [abbrev, in mathcomp.experimental_reals.distr]
dswap [def, in mathcomp.experimental_reals.distr]
dswapE [prf, in mathcomp.experimental_reals.distr]
dswapK [prf, 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.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_43 [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.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.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_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_g_dynkin [abbrev, in mathcomp.analysis.measure]
dynkin_lambda_system [prf, 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]