'D' (Lemmas)

Files

Definitions

Lemmas

Abbreviations

Global Index

D (Lemmas)

dadd [prf, in mathcomp.analysis.derive]
dadd0e_subproof [prf, in mathcomp.reals.constructive_ereal]
dadde_snum_subproof [prf, in mathcomp.reals.constructive_ereal]
daddeA_subproof [prf, in mathcomp.reals.constructive_ereal]
daddeC_subproof [prf, in mathcomp.reals.constructive_ereal]
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_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]
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]
dEFin_snum_subproof [prf, in mathcomp.reals.constructive_ereal]
deg_le2_ge0 [prf, in mathcomp.classical.mathcomp_extra]
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]
derivable1_diffP [prf, in mathcomp.analysis.derive]
derivable1P [prf, in mathcomp.analysis.derive]
derivable_cos [prf, in mathcomp.analysis.trigo]
derivable_cst [prf, in mathcomp.analysis.derive]
derivable_expR [prf, in mathcomp.analysis.exp]
derivable_id [prf, in mathcomp.analysis.derive]
derivable_nbhs [prf, in mathcomp.analysis.derive]
derivable_nbhsP [prf, in mathcomp.analysis.derive]
derivable_nbhsx [prf, in mathcomp.analysis.derive]
derivable_nbhsxP [prf, in mathcomp.analysis.derive]
derivable_oo_continuous_bnd_within [prf, in mathcomp.analysis.realfun]
derivable_sin [prf, in mathcomp.analysis.trigo]
derivable_sum [prf, in mathcomp.analysis.derive]
derivable_tan [prf, in mathcomp.analysis.trigo]
derivable_within_continuous [prf, in mathcomp.analysis.derive]
derivableB [prf, in mathcomp.analysis.derive]
derivableD [prf, in mathcomp.analysis.derive]
derivableM [prf, in mathcomp.analysis.derive]
derivableN [prf, in mathcomp.analysis.derive]
derivableP [prf, in mathcomp.analysis.derive]
derivableV [prf, in mathcomp.analysis.derive]
derivableX [prf, in mathcomp.analysis.derive]
derivableZ [prf, in mathcomp.analysis.derive]
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]
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]
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]
dflip1E [prf, in mathcomp.experimental_reals.distr]
dfstE [prf, in mathcomp.experimental_reals.distr]
dfwith_continuous [prf, in mathcomp.analysis.function_spaces]
dfwithin [prf, in mathcomp.classical.mathcomp_extra]
dfwithout [prf, in mathcomp.classical.mathcomp_extra]
dfwithP [prf, in mathcomp.classical.mathcomp_extra]
diagonalP [prf, in mathcomp.classical.classical_sets]
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]
diffB [prf, in mathcomp.analysis.derive]
diffD [prf, in mathcomp.analysis.derive]
diffE [prf, 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_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]
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]
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_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]
dirac0 [prf, in mathcomp.analysis.measure]
diracE [prf, in mathcomp.analysis.measure]
diracT [prf, in mathcomp.analysis.measure]
discrete_ball_center [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_bool [prf, in mathcomp.analysis.topology_theory.bool_topology]
discrete_bool_compact [prf, in mathcomp.analysis.topology_theory.bool_topology]
discrete_closed [prf, in mathcomp.analysis.topology_theory.topology_structure]
discrete_cvg [prf, in mathcomp.analysis.topology_theory.topology_structure]
discrete_hausdorff [prf, in mathcomp.analysis.separation_axioms]
discrete_measurable0 [prf, in mathcomp.analysis.measure]
discrete_measurableC [prf, in mathcomp.analysis.measure]
discrete_measurableU [prf, in mathcomp.analysis.measure]
discrete_nat [prf, in mathcomp.analysis.topology_theory.nat_topology]
discrete_nbhs [prf, in mathcomp.analysis.topology_theory.topology_structure]
discrete_open [prf, in mathcomp.analysis.topology_theory.topology_structure]
discrete_set1 [prf, in mathcomp.analysis.topology_theory.topology_structure]
discrete_sing [prf, in mathcomp.analysis.topology_theory.topology_structure]
discrete_space_discrete [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
discrete_zero_dimension [prf, in mathcomp.analysis.separation_axioms]
disj_itv_Rhull [prf, in mathcomp.analysis.normedtype]
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_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]
distribution_dRV [prf, in mathcomp.analysis.probability]
distribution_dRV_enum [prf, in mathcomp.analysis.probability]
dlet_additive [prf, in mathcomp.experimental_reals.distr]
dlet_dinsupp [prf, in mathcomp.experimental_reals.distr]
dlet_dunit_id [prf, in mathcomp.experimental_reals.distr]
dlet_eq0 [prf, 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]
dlim_ub [prf, in mathcomp.experimental_reals.distr]
dlimC [prf, in mathcomp.experimental_reals.distr]
dlimE [prf, in mathcomp.experimental_reals.distr]
dlimP [prf, in mathcomp.experimental_reals.distr]
dlin [prf, in mathcomp.analysis.derive]
dmargin_dunit [prf, in mathcomp.experimental_reals.distr]
dmargin_psumE [prf, in mathcomp.experimental_reals.distr]
dmarginE [prf, in mathcomp.experimental_reals.distr]
dnbhs0_le [prf, in mathcomp.analysis.normedtype]
dnbhs0_lt [prf, in mathcomp.analysis.normedtype]
dnbhs_ball [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
dnbhsE [prf, in mathcomp.analysis.topology_theory.topology_structure]
dnbhsN [prf, in mathcomp.analysis.normedtype]
dnullE [prf, in mathcomp.experimental_reals.distr]
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]
dopp [prf, in mathcomp.analysis.derive]
double_snum_subproof [prf, in mathcomp.reals.signed]
downK [prf, in mathcomp.reals.reals]
downP [prf, in mathcomp.classical.classical_sets]
dpair [prf, in mathcomp.analysis.derive]
drat1E [prf, in mathcomp.experimental_reals.distr]
drestrD [prf, in mathcomp.experimental_reals.distr]
drestrE [prf, in mathcomp.experimental_reals.distr]
dRV_dom_enum [prf, in mathcomp.analysis.probability]
dRV_expectation [prf, in mathcomp.analysis.probability]
dscale [prf, in mathcomp.analysis.derive]
dscalel [prf, in mathcomp.analysis.derive]
dswapE [prf, in mathcomp.experimental_reals.distr]
dswapK [prf, in mathcomp.experimental_reals.distr]
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.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.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_dDl [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.gee_dDr [prf, 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.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_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_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_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_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_le_dB [prf, in mathcomp.reals.constructive_ereal]
DualAddTheoryRealDomain.lte_le_dD [prf, 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.lee_daddgt0Pr [prf, in mathcomp.reals.constructive_ereal]
duni1E [prf, in mathcomp.experimental_reals.distr]
dunit1E [prf, in mathcomp.experimental_reals.distr]
dvg_approx [prf, in mathcomp.analysis.lebesgue_integral]
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]
dyadic_itv_image [prf, in mathcomp.analysis.lebesgue_integral]
dyadic_itv_subU [prf, in mathcomp.analysis.lebesgue_integral]
dynkin_lambda_system [prf, 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]