D (Definitions)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Notations |
D (Definitions)
davg [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]dcvg [def, in mathcomp.experimental_reals.distr]
decode [def, in mathcomp.reals.constructive_ereal]
dEFin [def, in mathcomp.reals.constructive_ereal]
dense [def, in mathcomp.analysis.topology_theory.topology_structure]
derivable [def, in mathcomp.analysis.derive]
derivable_Nyo_continuous_bnd [def, in mathcomp.analysis.realfun]
derivable_oo_continuous_bnd [def, in mathcomp.analysis.realfun]
derivable_oy_continuous_bnd [def, in mathcomp.analysis.realfun]
derive [def, in mathcomp.analysis.derive]
derive1 [def, in mathcomp.analysis.derive]
derive1n [def, in mathcomp.analysis.derive]
dflip [def, in mathcomp.experimental_reals.distr]
dfwith [def, in mathcomp.classical.mathcomp_extra]
diagonal [def, in mathcomp.classical.classical_sets]
diff [def, in mathcomp.analysis.derive]
dinsupp [def, in mathcomp.experimental_reals.distr]
dirac [def, in mathcomp.analysis.measure]
discontinuity [def, in mathcomp.analysis.realfun]
discrete_ball [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_ent [def, in mathcomp.analysis.topology_theory.discrete_topology]
discrete_measurable [def, in mathcomp.analysis.measure]
Discrete_ofNbhs.identity_builder [def, 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.identity_builder [def, 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.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_random_variable [def, in mathcomp.analysis.probability]
discrete_topology [def, in mathcomp.analysis.topology_theory.discrete_topology]
discreteMeasurableFun.pack_ [def, in mathcomp.analysis.probability]
discreteMeasurableFun.phant_clone [def, in mathcomp.analysis.probability]
discreteMeasurableFun.phant_on_ [def, in mathcomp.analysis.probability]
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]
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.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]
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.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_ofUniform.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.phant_Build [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.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]
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.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_ofNbhs.phant_axioms [def, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.phant_Build [def, in mathcomp.analysis.topology_theory.discrete_topology]
disj_set [def, in mathcomp.classical.classical_sets]
disjoint_itv [def, in mathcomp.classical.set_interval]
distr_of [def, in mathcomp.experimental_reals.distr]
distribution [def, in mathcomp.analysis.probability]
diter [def, in mathcomp.experimental_reals.distr]
dlet [def, in mathcomp.experimental_reals.distr]
dlift [def, in mathcomp.experimental_reals.distr]
dlim [def, in mathcomp.experimental_reals.distr]
dlim_bump [def, in mathcomp.experimental_reals.distr]
dlim_lift [def, in mathcomp.experimental_reals.distr]
dmargin [def, in mathcomp.experimental_reals.distr]
dnbhs [def, in mathcomp.analysis.topology_theory.topology_structure]
dnbhs_filter_on [def, in mathcomp.analysis.topology_theory.topology_structure]
dnull [def, in mathcomp.experimental_reals.distr]
dominated_by [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
double_snum [def, in mathcomp.reals.signed]
down [def, in mathcomp.classical.classical_sets]
drat [def, in mathcomp.experimental_reals.distr]
drestr [def, in mathcomp.experimental_reals.distr]
dRV_dom [def, in mathcomp.analysis.probability]
dRV_enum [def, in mathcomp.analysis.probability]
dswap [def, in mathcomp.experimental_reals.distr]
dual_adde [def, in mathcomp.reals.constructive_ereal]
dual_extended [def, in mathcomp.reals.constructive_ereal]
ducvg [def, in mathcomp.experimental_reals.distr]
duni [def, in mathcomp.experimental_reals.distr]
dunit [def, in mathcomp.experimental_reals.distr]
dyadic_approx [def, in mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation]
dyadic_itv [def, in mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation]
dynkin [def, in mathcomp.analysis.measure]