D (Abbreviations)
| 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 (Abbreviations)
derivable_Noy_continuous_within_itvNyc [abbrev, in mathcomp.analysis.realfun]derivable_Nyo_continuous_bnd [abbrev, in mathcomp.analysis.realfun]
derivable_oo_continuous_bnd [abbrev, in mathcomp.analysis.realfun]
derivable_oo_continuous_bnd_onemXnMr [abbrev, in mathcomp.analysis.probability]
derivable_oo_continuous_bnd_within [abbrev, in mathcomp.analysis.realfun]
derivable_oy_continuous_bnd [abbrev, in mathcomp.analysis.realfun]
derivable_oy_continuous_within_itvcy [abbrev, in mathcomp.analysis.realfun]
derivemxE [abbrev, in mathcomp.analysis.derive]
dfst [abbrev, in mathcomp.experimental_reals.distr]
dfst_dswap [abbrev, in mathcomp.experimental_reals.distr]
differentiable [abbrev, in mathcomp.analysis.derive]
differentiable [abbrev, in mathcomp.analysis.derive]
differentiable [abbrev, in mathcomp.analysis.derive]
Discrete_ofNbhs [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.axioms [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofNbhs.Build [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.axioms [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofPseudometric.Build [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.axioms [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
Discrete_ofUniform.Build [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
discreteMeasurableFun [abbrev, in mathcomp.analysis.probability]
discreteMeasurableFun.clone [abbrev, in mathcomp.analysis.probability]
discreteMeasurableFun.copy [abbrev, in mathcomp.analysis.probability]
discreteMeasurableFun.on [abbrev, in mathcomp.analysis.probability]
discreteMeasurableFun.on_ [abbrev, in mathcomp.analysis.probability]
DiscreteNbhs [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.clone [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.copy [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.Exports.discreteNbhsType [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.on [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteNbhs.on_ [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.clone [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.copy [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.Exports.discreteOrderTopologicalType [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.on [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteOrderTopology.on_ [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.clone [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.copy [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.Exports.discretePseudoMetricType [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.on [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric.on_ [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.axioms [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscretePseudoMetric_ofUniform.Build [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.clone [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.copy [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.Exports.discreteTopologicalType [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.on [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteTopology.on_ [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.clone [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.copy [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.Exports.discreteUniformType [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.on [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform.on_ [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.axioms [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
DiscreteUniform_ofNbhs.Build [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
distr [abbrev, in mathcomp.experimental_reals.distr]
distr [abbrev, in mathcomp.experimental_reals.distr]
dlet_dlet [abbrev, in mathcomp.experimental_reals.distr]
dlet_dmargin [abbrev, in mathcomp.experimental_reals.distr]
dlet_lim [abbrev, in mathcomp.experimental_reals.distr]
dlim_let [abbrev, in mathcomp.experimental_reals.distr]
dmargin_dlet [abbrev, in mathcomp.experimental_reals.distr]
dominates_charge_variation [abbrev, in mathcomp.analysis.charge]
dsnd [abbrev, in mathcomp.experimental_reals.distr]
dsnd_dswap [abbrev, in mathcomp.experimental_reals.distr]
dsndE [abbrev, in mathcomp.experimental_reals.distr]
DualAddTheoryNumDomain.gte_dopp [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gee_daddl [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gee_daddr [abbrev, 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_dsubl [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gte_dsubr [abbrev, 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_dsub [abbrev, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lee_lt_dadd [abbrev, 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_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_dsub [abbrev, in mathcomp.reals.constructive_ereal]
dweight [abbrev, in mathcomp.experimental_reals.distr]