'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 | _ | * |
D (Abbreviations)
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]
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]
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]
dvg_ereal_cvg [abbrev, in mathcomp.analysis.sequences]
dweight [abbrev, in mathcomp.experimental_reals.distr]
dynkin_g_dynkin [abbrev, in mathcomp.analysis.measure]
dynkin_monotone [abbrev, in mathcomp.analysis.measure]