'E' (Lemmas)
| 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 | _ | * |
E (Lemmas)
eclamp_id [prf, in mathcomp.analysis.altreals.realseq]ecvg_approx [prf, in mathcomp.analysis.lebesgue_integral]
edist_closel [prf, in mathcomp.analysis.normedtype]
edist_closeP [prf, in mathcomp.analysis.normedtype]
edist_continuous [prf, in mathcomp.analysis.normedtype]
edist_fin [prf, in mathcomp.analysis.normedtype]
edist_fin_closed [prf, in mathcomp.analysis.normedtype]
edist_fin_open [prf, in mathcomp.analysis.normedtype]
edist_finP [prf, in mathcomp.analysis.normedtype]
edist_ge0 [prf, in mathcomp.analysis.normedtype]
edist_inf0 [prf, in mathcomp.analysis.normedtype]
edist_inf_continuous [prf, in mathcomp.analysis.normedtype]
edist_inf_ge0 [prf, in mathcomp.analysis.normedtype]
edist_inf_neqNy [prf, in mathcomp.analysis.normedtype]
edist_inf_triangle [prf, in mathcomp.analysis.normedtype]
edist_lt_ball [prf, in mathcomp.analysis.normedtype]
edist_neqNy [prf, in mathcomp.analysis.normedtype]
edist_pinfty_open [prf, in mathcomp.analysis.normedtype]
edist_pinftyP [prf, in mathcomp.analysis.normedtype]
edist_refl [prf, in mathcomp.analysis.normedtype]
edist_sym [prf, in mathcomp.analysis.normedtype]
edist_triangle [prf, in mathcomp.analysis.normedtype]
EFin_bigcup [prf, in mathcomp.analysis.ereal]
EFin_expe [prf, in mathcomp.analysis.constructive_ereal]
EFin_inj [prf, in mathcomp.analysis.constructive_ereal]
EFin_itv [prf, in mathcomp.analysis.lebesgue_measure]
EFin_itv_bnd_infty [prf, in mathcomp.analysis.lebesgue_measure]
EFin_lim [prf, in mathcomp.analysis.normedtype]
EFin_max [prf, in mathcomp.analysis.constructive_ereal]
EFin_measurable [prf, in mathcomp.analysis.lebesgue_measure]
EFin_min [prf, in mathcomp.analysis.constructive_ereal]
EFin_natmul [prf, in mathcomp.analysis.constructive_ereal]
EFin_normr_Rintegral [prf, in mathcomp.analysis.lebesgue_integral]
EFin_semi_additive [prf, in mathcomp.analysis.constructive_ereal]
EFin_setC [prf, in mathcomp.analysis.ereal]
EFin_snum_subproof [prf, in mathcomp.analysis.constructive_ereal]
EFin_sum_fine [prf, in mathcomp.analysis.constructive_ereal]
EFinB [prf, in mathcomp.analysis.constructive_ereal]
EFinD [prf, in mathcomp.analysis.constructive_ereal]
EFinM [prf, in mathcomp.analysis.constructive_ereal]
EFinN [prf, in mathcomp.analysis.constructive_ereal]
einfs_le_esups [prf, in mathcomp.analysis.sequences]
einfs_preimage [prf, in mathcomp.analysis.sequences]
einfsN [prf, in mathcomp.analysis.sequences]
eitv_bnd_infty [prf, in mathcomp.analysis.lebesgue_measure]
eitv_infty_bnd [prf, in mathcomp.analysis.lebesgue_measure]
elebesgue_measure0 [prf, in mathcomp.analysis.lebesgue_measure]
elebesgue_measure_ge0 [prf, in mathcomp.analysis.lebesgue_measure]
EM [prf, in mathcomp.classical.boolp]
emeasurable0 [prf, in mathcomp.analysis.lebesgue_measure]
emeasurable_fin_num [prf, in mathcomp.analysis.lebesgue_measure]
emeasurable_fun_c_infty [prf, in mathcomp.analysis.lebesgue_measure]
emeasurable_fun_cvg [prf, in mathcomp.analysis.lebesgue_measure]
emeasurable_fun_eq [prf, in mathcomp.analysis.lebesgue_integral]
emeasurable_fun_fsum [prf, in mathcomp.analysis.lebesgue_integral]
emeasurable_fun_infty_c [prf, in mathcomp.analysis.lebesgue_measure]
emeasurable_fun_infty_o [prf, in mathcomp.analysis.lebesgue_measure]
emeasurable_fun_le [prf, in mathcomp.analysis.lebesgue_integral]
emeasurable_fun_lt [prf, in mathcomp.analysis.lebesgue_integral]
emeasurable_fun_neq [prf, in mathcomp.analysis.lebesgue_integral]
emeasurable_fun_o_infty [prf, in mathcomp.analysis.lebesgue_measure]
emeasurable_fun_sum [prf, in mathcomp.analysis.lebesgue_integral]
emeasurable_funB [prf, in mathcomp.analysis.lebesgue_integral]
emeasurable_funD [prf, in mathcomp.analysis.lebesgue_integral]
emeasurable_funM [prf, in mathcomp.analysis.lebesgue_integral]
emeasurable_itv [prf, in mathcomp.analysis.lebesgue_measure]
emeasurable_neq [prf, in mathcomp.analysis.lebesgue_measure]
emeasurable_set1 [prf, in mathcomp.analysis.lebesgue_measure]
emeasurableC [prf, in mathcomp.analysis.lebesgue_measure]
empty_can_subproof [prf, in mathcomp.classical.functions]
empty_canv_subproof [prf, in mathcomp.classical.functions]
empty_eq0 [prf, in mathcomp.classical.classical_sets]
empty_eq0 [prf, in mathcomp.classical.cardinality]
empty_fun_subproof [prf, in mathcomp.classical.functions]
enatmul_ninfty [prf, in mathcomp.analysis.constructive_ereal]
enatmul_pinfty [prf, in mathcomp.analysis.constructive_ereal]
ent_closure [prf, in mathcomp.analysis.topology_theory.uniform_structure]
entourage_ball [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
entourage_ballE [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
entourage_close [prf, in mathcomp.analysis.separation_axioms]
entourage_E [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
entourage_from_ballE [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
entourage_inv [prf, in mathcomp.analysis.topology_theory.uniform_structure]
entourage_invI [prf, in mathcomp.analysis.topology_theory.uniform_structure]
entourage_refl [prf, in mathcomp.analysis.topology_theory.uniform_structure]
entourage_split [prf, in mathcomp.analysis.topology_theory.uniform_structure]
entourage_split_ent [prf, in mathcomp.analysis.topology_theory.uniform_structure]
entourage_split_ex [prf, in mathcomp.analysis.topology_theory.uniform_structure]
entourage_sym [prf, in mathcomp.analysis.topology_theory.uniform_structure]
entourageT [prf, in mathcomp.analysis.topology_theory.uniform_structure]
enum_fset0 [prf, in mathcomp.analysis.altreals.xfinmap]
enum_fset1 [prf, in mathcomp.analysis.altreals.xfinmap]
enum_fsetT [prf, in mathcomp.analysis.altreals.xfinmap]
epatch_indic [prf, in mathcomp.analysis.numfun]
epiP [prf, in mathcomp.classical.functions]
epsilon_trick [prf, in mathcomp.analysis.measure]
epsilon_trick0 [prf, in mathcomp.analysis.measure]
eq0 [prf, in mathcomp.analysis.signed]
eq0_dlet [prf, in mathcomp.analysis.altreals.distr]
eq0_pr [prf, in mathcomp.analysis.altreals.distr]
eq0_prc [prf, in mathcomp.analysis.altreals.distr]
eq0_psum [prf, in mathcomp.analysis.altreals.realsum]
eq0F [prf, in mathcomp.analysis.signed]
eq_bigcap [prf, in mathcomp.classical.classical_sets]
eq_bigcapl [prf, in mathcomp.classical.classical_sets]
eq_bigcapr [prf, in mathcomp.classical.classical_sets]
eq_bigcup [prf, in mathcomp.classical.classical_sets]
eq_bigcup_seqD [prf, in mathcomp.analysis.sequences]
eq_bigcup_seqD_bigsetU [prf, in mathcomp.analysis.sequences]
eq_bigcupl [prf, in mathcomp.classical.classical_sets]
eq_bigcupr [prf, in mathcomp.classical.classical_sets]
eq_card1 [prf, in mathcomp.classical.cardinality]
eq_card_fset_subset [prf, in mathcomp.classical.cardinality]
eq_card_nat [prf, in mathcomp.classical.cardinality]
eq_cardSP [prf, in mathcomp.classical.cardinality]
eq_countable [prf, in mathcomp.classical.cardinality]
eq_cvg [prf, in mathcomp.classical.filter]
eq_dlim [prf, in mathcomp.analysis.altreals.distr]
eq_eseriesl [prf, in mathcomp.analysis.sequences]
eq_eseriesr [prf, in mathcomp.analysis.sequences]
eq_esum [prf, in mathcomp.analysis.esum]
eq_exist [prf, in mathcomp.classical.boolp]
eq_exists [prf, in mathcomp.classical.boolp]
eq_exists2 [prf, in mathcomp.classical.boolp]
eq_exists3 [prf, in mathcomp.classical.boolp]
eq_exp [prf, in mathcomp.analysis.altreals.distr]
eq_finite_set [prf, in mathcomp.classical.cardinality]
eq_finite_support [prf, in mathcomp.classical.fsbigop]
eq_fneg [prf, in mathcomp.analysis.altreals.realsum]
eq_forall [prf, in mathcomp.classical.boolp]
eq_forall2 [prf, in mathcomp.classical.boolp]
eq_forall3 [prf, in mathcomp.classical.boolp]
eq_fpos [prf, in mathcomp.analysis.altreals.realsum]
eq_from_dlim [prf, in mathcomp.analysis.altreals.distr]
eq_from_nlim [prf, in mathcomp.analysis.altreals.realseq]
eq_fsbigl [prf, in mathcomp.classical.fsbigop]
eq_fsbigr [prf, in mathcomp.classical.fsbigop]
eq_fun [prf, in mathcomp.classical.boolp]
eq_fun2 [prf, in mathcomp.classical.boolp]
eq_fun3 [prf, in mathcomp.classical.boolp]
eq_image_id [prf, in mathcomp.classical.classical_sets]
eq_imageK [prf, in mathcomp.classical.classical_sets]
eq_imagel [prf, in mathcomp.classical.classical_sets]
eq_in_close [prf, in mathcomp.analysis.function_spaces]
eq_in_dlet [prf, in mathcomp.analysis.altreals.distr]
eq_in_pr [prf, in mathcomp.analysis.altreals.distr]
eq_index_bmaxrf [prf, in mathcomp.analysis.Rstruct]
eq_infty [prf, in mathcomp.analysis.constructive_ereal]
eq_integrable [prf, in mathcomp.analysis.lebesgue_integral]
eq_integral [prf, in mathcomp.analysis.lebesgue_integral]
eq_integral_itv_bounded [prf, in mathcomp.analysis.lebesgue_integral]
eq_is_cvg [prf, in mathcomp.classical.filter]
eq_is_cvg_in [prf, in mathcomp.classical.filter]
eq_kernel [prf, in mathcomp.analysis.kernel]
eq_Lnorm [prf, in mathcomp.analysis.hoelder]
eq_map_mx_id [prf, in mathcomp.analysis.forms]
eq_measurable_fun [prf, in mathcomp.analysis.measure]
eq_measure [prf, in mathcomp.analysis.measure]
eq_measure_integral [prf, in mathcomp.analysis.lebesgue_integral]
eq_measureU [prf, in mathcomp.analysis.measure]
eq_near [prf, in mathcomp.classical.filter]
eq_ninfty [prf, in mathcomp.analysis.constructive_ereal]
eq_nlim [prf, in mathcomp.analysis.altreals.realseq]
eq_opE [prf, in mathcomp.classical.boolp]
eq_ppsum [prf, in mathcomp.analysis.altreals.realsum]
eq_pr [prf, in mathcomp.analysis.altreals.distr]
eq_preimage [prf, in mathcomp.classical.classical_sets]
eq_psum [prf, in mathcomp.analysis.altreals.realsum]
eq_psum_abs [prf, in mathcomp.analysis.altreals.realsum]
eq_restrictP [prf, in mathcomp.classical.functions]
eq_Rintegral [prf, in mathcomp.analysis.lebesgue_integral]
eq_set [prf, in mathcomp.classical.classical_sets]
eq_set_bij [prf, in mathcomp.classical.functions]
eq_set_bijLR [prf, in mathcomp.classical.functions]
eq_set_bijRL [prf, in mathcomp.classical.functions]
eq_sfkernel [prf, in mathcomp.analysis.kernel]
eq_sigLfunP [prf, in mathcomp.classical.functions]
eq_sigLP [prf, in mathcomp.classical.functions]
eq_sintegral [prf, in mathcomp.analysis.lebesgue_integral]
eq_some_OP [prf, in mathcomp.analysis.landau]
eq_some_oP [prf, in mathcomp.analysis.landau]
eq_sum [prf, in mathcomp.analysis.altreals.realsum]
eq_sum_telescope [prf, in mathcomp.analysis.sequences]
eq_summable [prf, in mathcomp.analysis.altreals.realsum]
eq_summableb [prf, in mathcomp.analysis.altreals.realsum]
eqadd_some_OP [prf, in mathcomp.analysis.landau]
eqadd_some_oP [prf, in mathcomp.analysis.landau]
eqaddO_trans [prf, in mathcomp.analysis.landau]
eqaddo_trans [prf, in mathcomp.analysis.landau]
eqaddOE [prf, in mathcomp.analysis.landau]
eqaddoE [prf, in mathcomp.analysis.landau]
eqaddOEx [prf, in mathcomp.analysis.landau]
eqaddoEx [prf, in mathcomp.analysis.landau]
eqaddOo_trans [prf, in mathcomp.analysis.landau]
eqaddoO_trans [prf, in mathcomp.analysis.landau]
eqaddOP [prf, in mathcomp.analysis.landau]
eqaddoP [prf, in mathcomp.analysis.landau]
eqcover_r [prf, in mathcomp.classical.classical_sets]
eqe [prf, in mathcomp.analysis.constructive_ereal]
eqe_absl [prf, in mathcomp.analysis.constructive_ereal]
eqe_opp [prf, in mathcomp.analysis.constructive_ereal]
eqe_oppLR [prf, in mathcomp.analysis.constructive_ereal]
eqe_oppLRP [prf, in mathcomp.analysis.constructive_ereal]
eqe_oppP [prf, in mathcomp.analysis.constructive_ereal]
eqe_pdivrMl [prf, in mathcomp.analysis.constructive_ereal]
eqEsubset [prf, in mathcomp.classical.classical_sets]
eqincl_surj [prf, in mathcomp.classical.functions]
eqO_bigO [prf, in mathcomp.analysis.landau]
eqO_exP [prf, in mathcomp.analysis.landau]
eqo_pair [prf, in mathcomp.analysis.derive]
eqO_trans [prf, in mathcomp.analysis.landau]
eqo_trans [prf, in mathcomp.analysis.landau]
eqoaddo [prf, in mathcomp.analysis.landau]
eqOE [prf, in mathcomp.analysis.landau]
eqoE [prf, in mathcomp.analysis.landau]
eqOEx [prf, in mathcomp.analysis.landau]
eqoEx [prf, in mathcomp.analysis.landau]
eqolim [prf, in mathcomp.analysis.landau]
eqolim0 [prf, in mathcomp.analysis.landau]
eqolim0P [prf, in mathcomp.analysis.landau]
eqolimP [prf, in mathcomp.analysis.landau]
eqOmega_trans [prf, in mathcomp.analysis.landau]
eqOmegaE [prf, in mathcomp.analysis.landau]
eqOmegaO [prf, in mathcomp.analysis.landau]
eqoO [prf, in mathcomp.analysis.landau]
eqoO_trans [prf, in mathcomp.analysis.landau]
eqOo_trans [prf, in mathcomp.analysis.landau]
eqOP [prf, in mathcomp.analysis.landau]
eqoP [prf, in mathcomp.analysis.landau]
eqPchoice [prf, in mathcomp.classical.boolp]
eqPcountable [prf, in mathcomp.classical.cardinality]
eqPpointed [prf, in mathcomp.classical.classical_sets]
eqr_div [prf, in mathcomp.analysis.trigo]
eqrP [prf, in mathcomp.analysis.Rstruct]
eqTheta_trans [prf, in mathcomp.analysis.landau]
eqThetaE [prf, in mathcomp.analysis.landau]
eqThetaO [prf, in mathcomp.analysis.landau]
equicontinuous_closure [prf, in mathcomp.analysis.function_spaces]
equicontinuous_continuous [prf, in mathcomp.analysis.function_spaces]
equicontinuous_continuous_for [prf, in mathcomp.analysis.function_spaces]
equicontinuous_subset [prf, in mathcomp.analysis.function_spaces]
equicontinuous_subset_id [prf, in mathcomp.analysis.function_spaces]
equiv_refl [prf, in mathcomp.analysis.landau]
equiv_sym [prf, in mathcomp.analysis.landau]
equiv_trans [prf, in mathcomp.analysis.landau]
equivalence_rel_equiv [prf, in mathcomp.analysis.landau]
equivoLR [prf, in mathcomp.analysis.landau]
equivOLR [prf, in mathcomp.analysis.landau]
equivORL [prf, in mathcomp.analysis.landau]
equivoRL [prf, in mathcomp.analysis.landau]
eqy_poweR [prf, in mathcomp.analysis.exp]
eqyP [prf, in mathcomp.analysis.constructive_ereal]
er_map_idfun [prf, in mathcomp.analysis.constructive_ereal]
ereal_ball_center [prf, in mathcomp.analysis.constructive_ereal]
ereal_ball_ninfty_oversize [prf, in mathcomp.analysis.constructive_ereal]
ereal_ball_sym [prf, in mathcomp.analysis.constructive_ereal]
ereal_ball_triangle [prf, in mathcomp.analysis.constructive_ereal]
ereal_ballN [prf, in mathcomp.analysis.constructive_ereal]
ereal_comparable [prf, in mathcomp.analysis.constructive_ereal]
ereal_display [prf, in mathcomp.analysis.constructive_ereal]
ereal_dnbhs_le [prf, in mathcomp.analysis.ereal]
ereal_dnbhs_le_finite [prf, in mathcomp.analysis.ereal]
ereal_eqP [prf, in mathcomp.analysis.constructive_ereal]
ereal_hausdorff [prf, in mathcomp.analysis.normedtype]
ereal_inf0 [prf, in mathcomp.analysis.ereal]
ereal_inf1 [prf, in mathcomp.analysis.ereal]
ereal_inf_EFin [prf, in mathcomp.analysis.ereal]
ereal_inf_lbound [prf, in mathcomp.analysis.ereal]
ereal_inf_le [prf, in mathcomp.analysis.ereal]
ereal_inf_lt [prf, in mathcomp.analysis.ereal]
ereal_inf_pinfty [prf, in mathcomp.analysis.ereal]
ereal_inf_snum_subproof [prf, in mathcomp.analysis.ereal]
ereal_infT [prf, in mathcomp.analysis.ereal]
ereal_mem_Interval [prf, in mathcomp.analysis.real_interval]
ereal_nbhs_nbhs [prf, in mathcomp.analysis.ereal]
ereal_nbhs_ninfty_le [prf, in mathcomp.analysis.ereal]
ereal_nbhs_ninfty_lt [prf, in mathcomp.analysis.ereal]
ereal_nbhs_ninfty_real [prf, in mathcomp.analysis.ereal]
ereal_nbhs_pinfty_ge [prf, in mathcomp.analysis.ereal]
ereal_nbhs_pinfty_gt [prf, in mathcomp.analysis.ereal]
ereal_nbhs_pinfty_real [prf, in mathcomp.analysis.ereal]
ereal_nbhs_singleton [prf, in mathcomp.analysis.ereal]
ereal_nbhsE [prf, in mathcomp.analysis.ereal]
ereal_nondecreasing_cvgn [prf, in mathcomp.analysis.sequences]
ereal_nondecreasing_is_cvgn [prf, in mathcomp.analysis.sequences]
ereal_nondecreasing_oppn [prf, in mathcomp.analysis.sequences]
ereal_nondecreasing_series [prf, in mathcomp.analysis.sequences]
ereal_nonincreasing_cvgn [prf, in mathcomp.analysis.sequences]
ereal_nonincreasing_is_cvgn [prf, in mathcomp.analysis.sequences]
ereal_series [prf, in mathcomp.analysis.sequences]
ereal_series_cond [prf, in mathcomp.analysis.sequences]
ereal_sup0 [prf, in mathcomp.analysis.ereal]
ereal_sup1 [prf, in mathcomp.analysis.ereal]
ereal_sup_EFin [prf, in mathcomp.analysis.ereal]
ereal_sup_gt [prf, in mathcomp.analysis.ereal]
ereal_sup_le [prf, in mathcomp.analysis.ereal]
ereal_sup_ninfty [prf, in mathcomp.analysis.ereal]
ereal_sup_snum_subproof [prf, in mathcomp.analysis.ereal]
ereal_sup_ubound [prf, in mathcomp.analysis.ereal]
ereal_supremums_neq0 [prf, in mathcomp.analysis.ereal]
ereal_supremums_set0_ninfty [prf, in mathcomp.analysis.ereal]
ereal_supT [prf, in mathcomp.analysis.ereal]
ereal_supy [prf, in mathcomp.analysis.ereal]
ereal_ub_ninfty [prf, in mathcomp.analysis.ereal]
ereal_ub_pinfty [prf, in mathcomp.analysis.ereal]
ErealGenCInfty.measurable_set1Ny [prf, in mathcomp.analysis.lebesgue_measure]
ErealGenCInfty.measurable_set1y [prf, in mathcomp.analysis.lebesgue_measure]
ErealGenCInfty.measurableE [prf, in mathcomp.analysis.lebesgue_measure]
ErealGenInftyO.measurableE [prf, in mathcomp.analysis.lebesgue_measure]
ErealGenOInfty.measurable_set1Ny [prf, in mathcomp.analysis.lebesgue_measure]
ErealGenOInfty.measurable_set1y [prf, in mathcomp.analysis.lebesgue_measure]
ErealGenOInfty.measurableE [prf, in mathcomp.analysis.lebesgue_measure]
erestrict0 [prf, in mathcomp.analysis.numfun]
erestrict_ge0 [prf, in mathcomp.analysis.numfun]
erestrict_scale [prf, in mathcomp.analysis.numfun]
erestrict_set0 [prf, in mathcomp.analysis.numfun]
erestrictB [prf, in mathcomp.analysis.numfun]
erestrictD [prf, in mathcomp.analysis.numfun]
erestrictM [prf, in mathcomp.analysis.numfun]
erestrictN [prf, in mathcomp.analysis.numfun]
eseries0 [prf, in mathcomp.analysis.sequences]
eseries_addn [prf, in mathcomp.analysis.sequences]
eseries_cond [prf, in mathcomp.analysis.sequences]
eseries_mkcond [prf, in mathcomp.analysis.sequences]
eseries_mkcondl [prf, in mathcomp.analysis.sequences]
eseries_mkcondr [prf, in mathcomp.analysis.sequences]
eseries_pinfty [prf, in mathcomp.analysis.sequences]
eseries_pred0 [prf, in mathcomp.analysis.sequences]
eseriesD [prf, in mathcomp.analysis.sequences]
eseriesEnat [prf, in mathcomp.analysis.sequences]
eseriesEord [prf, in mathcomp.analysis.sequences]
eseriesS [prf, in mathcomp.analysis.sequences]
eseriesSB [prf, in mathcomp.analysis.sequences]
eseriesSr [prf, in mathcomp.analysis.sequences]
eset1Ny [prf, in mathcomp.analysis.lebesgue_measure]
eset1y [prf, in mathcomp.analysis.lebesgue_measure]
ess_sup_ge0 [prf, in mathcomp.analysis.measure]
esum1 [prf, in mathcomp.analysis.esum]
esum_bigcup [prf, in mathcomp.analysis.esum]
esum_bigcupT [prf, in mathcomp.analysis.esum]
esum_eqNy [prf, in mathcomp.analysis.constructive_ereal]
esum_eqNyP [prf, in mathcomp.analysis.constructive_ereal]
esum_eqy [prf, in mathcomp.analysis.constructive_ereal]
esum_eqyP [prf, in mathcomp.analysis.constructive_ereal]
esum_esum [prf, in mathcomp.analysis.esum]
esum_fset [prf, in mathcomp.analysis.esum]
esum_ge [prf, in mathcomp.analysis.esum]
esum_ge0 [prf, in mathcomp.analysis.esum]
esum_image [prf, in mathcomp.analysis.esum]
esum_mkcond [prf, in mathcomp.analysis.esum]
esum_mkcondl [prf, in mathcomp.analysis.esum]
esum_mkcondr [prf, in mathcomp.analysis.esum]
esum_pred_image [prf, in mathcomp.analysis.esum]
esum_set0 [prf, in mathcomp.analysis.esum]
esum_set1 [prf, in mathcomp.analysis.esum]
esum_set_image [prf, in mathcomp.analysis.esum]
esum_sum [prf, in mathcomp.analysis.esum]
esumB [prf, in mathcomp.analysis.esum]
esumD [prf, in mathcomp.analysis.esum]
esumID [prf, in mathcomp.analysis.esum]
esups_preimage [prf, in mathcomp.analysis.sequences]
esupsN [prf, in mathcomp.analysis.sequences]
EVT_max [prf, in mathcomp.analysis.derive]
EVT_min [prf, in mathcomp.analysis.derive]
ex_ball_sig [prf, in mathcomp.analysis.normedtype]
ex_bound [prf, in mathcomp.analysis.normedtype]
ex_dom_bound [prf, in mathcomp.analysis.normedtype]
ex_maximal_disjoint_subcollection [prf, in mathcomp.classical.classical_sets]
ex_strict_bound [prf, in mathcomp.analysis.normedtype]
ex_strict_bound_gt0 [prf, in mathcomp.analysis.normedtype]
ex_strict_dom_bound [prf, in mathcomp.analysis.normedtype]
ex_vitali_collection_partition [prf, in mathcomp.analysis.normedtype]
exchange_fsbig [prf, in mathcomp.classical.fsbigop]
exists2E [prf, in mathcomp.classical.boolp]
exists2P [prf, in mathcomp.classical.boolp]
exists_asboolP [prf, in mathcomp.classical.boolp]
exists_swap [prf, in mathcomp.classical.boolp]
existsNE [prf, in mathcomp.classical.boolp]
existsNP [prf, in mathcomp.classical.boolp]
existsp_asboolPn [prf, in mathcomp.classical.boolp]
existsPNP [prf, in mathcomp.classical.boolp]
existsTP [prf, in mathcomp.analysis.altreals.discrete]
exp0 [prf, in mathcomp.analysis.altreals.distr]
exp_coeff_ge0 [prf, in mathcomp.analysis.sequences]
exp_coeffE [prf, in mathcomp.analysis.exp]
exp_cst [prf, in mathcomp.analysis.altreals.distr]
exp_derive [prf, in mathcomp.analysis.derive]
exp_derive1 [prf, in mathcomp.analysis.derive]
exp_dunit [prf, in mathcomp.analysis.altreals.distr]
exp_le_bd [prf, in mathcomp.analysis.altreals.distr]
expand0 [prf, in mathcomp.analysis.constructive_ereal]
expand1 [prf, in mathcomp.analysis.constructive_ereal]
expand_eqNoo [prf, in mathcomp.analysis.constructive_ereal]
expand_eqoo [prf, in mathcomp.analysis.constructive_ereal]
expand_ereal_ball_fin_lt [prf, in mathcomp.analysis.ereal]
expand_ereal_ball_pinfty [prf, in mathcomp.analysis.ereal]
expandK [prf, in mathcomp.analysis.constructive_ereal]
expandN [prf, in mathcomp.analysis.constructive_ereal]
expandN1 [prf, in mathcomp.analysis.constructive_ereal]
expe2 [prf, in mathcomp.analysis.constructive_ereal]
expectation_cst [prf, in mathcomp.analysis.probability]
expectation_fin_num [prf, in mathcomp.analysis.probability]
expectation_ge0 [prf, in mathcomp.analysis.probability]
expectation_indic [prf, in mathcomp.analysis.probability]
expectation_le [prf, in mathcomp.analysis.probability]
expectation_pmf [prf, in mathcomp.analysis.probability]
expectation_sum [prf, in mathcomp.analysis.probability]
expectationB [prf, in mathcomp.analysis.probability]
expectationD [prf, in mathcomp.analysis.probability]
expectationM [prf, in mathcomp.analysis.probability]
expeR0 [prf, in mathcomp.analysis.exp]
expeR_eq0 [prf, in mathcomp.analysis.exp]
expeR_ge0 [prf, in mathcomp.analysis.exp]
expeR_ge1Dx [prf, in mathcomp.analysis.exp]
expeR_gt0 [prf, in mathcomp.analysis.exp]
expeR_inj [prf, in mathcomp.analysis.exp]
expeR_total [prf, in mathcomp.analysis.exp]
expeRD [prf, in mathcomp.analysis.exp]
expeS [prf, in mathcomp.analysis.constructive_ereal]
expn_snum_subproof [prf, in mathcomp.analysis.signed]
expR0 [prf, in mathcomp.analysis.exp]
expR0 [prf, in mathcomp.analysis.Rstruct]
expR_eq0 [prf, in mathcomp.analysis.exp]
expR_ge0 [prf, in mathcomp.analysis.exp]
expR_ge1Dx [prf, in mathcomp.analysis.exp]
expR_ge1Dx_subproof [prf, in mathcomp.analysis.exp]
expR_gt0 [prf, in mathcomp.analysis.exp]
expR_gt1 [prf, in mathcomp.analysis.exp]
expR_gt1Dx [prf, in mathcomp.analysis.exp]
expR_inj [prf, in mathcomp.analysis.exp]
expR_lt1 [prf, in mathcomp.analysis.exp]
expR_total [prf, in mathcomp.analysis.exp]
expR_total_gt1 [prf, in mathcomp.analysis.exp]
expRB [prf, in mathcomp.analysis.exp]
expRD [prf, in mathcomp.analysis.exp]
expRD [prf, in mathcomp.analysis.Rstruct]
expRE [prf, in mathcomp.analysis.exp]
exprfctE [prf, in mathcomp.classical.functions]
expRK [prf, in mathcomp.analysis.exp]
expRM [prf, in mathcomp.analysis.exp]
expRM_natl [prf, in mathcomp.analysis.exp]
expRM_natr [prf, in mathcomp.analysis.exp]
expRN [prf, in mathcomp.analysis.exp]
exprn_continuous [prf, in mathcomp.analysis.realfun]
exprn_derivable [prf, in mathcomp.analysis.derive]
exprn_geometric [prf, in mathcomp.analysis.sequences]
exprn_measurable [prf, in mathcomp.analysis.lebesgue_measure]
exprn_snum_subproof [prf, in mathcomp.analysis.signed]
expRX [prf, in mathcomp.analysis.Rstruct]
expRxDyMexpx [prf, in mathcomp.analysis.exp]
expRxMexpNx_1 [prf, in mathcomp.analysis.exp]
expZ [prf, in mathcomp.analysis.altreals.distr]
extensionality [prf, in mathcomp.classical.boolp]