L (Lemmas)

Files

Definitions

Lemmas

Abbreviations

Global Index

L (Lemmas)

L_iso [prf, in mathcomp.solvable.burnside_app]
Lagrange [prf, in mathcomp.finite_group.fingroup]
lagrange_coords [prf, in mathcomp.algebra.qpoly]
lagrange_free [prf, in mathcomp.algebra.qpoly]
lagrange_full [prf, in mathcomp.algebra.qpoly]
lagrange_gen [prf, in mathcomp.algebra.qpoly]
Lagrange_index [prf, in mathcomp.finite_group.fingroup]
lagrange_key [prf, in mathcomp.algebra.qpoly]
lagrange_sample [prf, in mathcomp.algebra.qpoly]
lagrangeE [prf, in mathcomp.algebra.qpoly]
LagrangeI [prf, in mathcomp.finite_group.fingroup]
LagrangeMl [prf, in mathcomp.finite_group.fingroup]
LagrangeMr [prf, in mathcomp.finite_group.fingroup]
lambda_system_smallest [prf, in mathcomp.analysis.measure_theory.measurable_structure]
lambda_system_subset [prf, in mathcomp.analysis.measure_theory.measurable_structure]
large_field_PET [prf, in mathcomp.field.separable]
last_cat [prf, in mathcomp.boot.seq]
last_cons [prf, in mathcomp.boot.seq]
last_drop [prf, in mathcomp.boot.seq]
last_eq [prf, in mathcomp.boot.seq]
last_filterP [prf, in mathcomp.classical.unstable]
last_ind [prf, in mathcomp.boot.seq]
last_map [prf, in mathcomp.boot.seq]
last_nth [prf, in mathcomp.boot.seq]
last_rcons [prf, in mathcomp.boot.seq]
last_take [prf, in mathcomp.boot.seq]
last_traject [prf, in mathcomp.boot.path]
lastI [prf, in mathcomp.boot.seq]
lastP [prf, in mathcomp.boot.seq]
lb_ereal_inf_adherent [prf, in mathcomp.analysis.ereal]
lb_ereal_infNy_adherent [prf, in mathcomp.analysis.ereal]
lb_le_inf [prf, in mathcomp.reals.reals]
lb_set1 [prf, in mathcomp.classical.classical_sets]
lb_ub_lb [prf, in mathcomp.classical.classical_sets]
lb_ub_refl [prf, in mathcomp.classical.classical_sets]
lb_ub_set1 [prf, in mathcomp.classical.classical_sets]
lb_ubN [prf, in mathcomp.classical.set_interval]
lboundT [prf, in mathcomp.reals.reals]
lbP [prf, in mathcomp.classical.classical_sets]
lcm0n [prf, in mathcomp.boot.div]
lcm0z [prf, in mathcomp.algebra.intdiv]
lcm1n [prf, in mathcomp.boot.div]
lcmn0 [prf, in mathcomp.boot.div]
lcmn1 [prf, in mathcomp.boot.div]
lcmn_gt0 [prf, in mathcomp.boot.div]
lcmn_idPl [prf, in mathcomp.boot.div]
lcmn_idPr [prf, in mathcomp.boot.div]
lcmnA [prf, in mathcomp.boot.div]
lcmnAC [prf, in mathcomp.boot.div]
lcmnACA [prf, in mathcomp.boot.div]
lcmnC [prf, in mathcomp.boot.div]
lcmnCA [prf, in mathcomp.boot.div]
lcmnMl [prf, in mathcomp.boot.div]
lcmnMr [prf, in mathcomp.boot.div]
lcmz0 [prf, in mathcomp.algebra.intdiv]
lcmz_ge0 [prf, in mathcomp.algebra.intdiv]
lcmz_neq0 [prf, in mathcomp.algebra.intdiv]
lcmzC [prf, in mathcomp.algebra.intdiv]
lcn0 [prf, in mathcomp.solvable.nilpotent]
lcn1 [prf, in mathcomp.solvable.nilpotent]
lcn2 [prf, in mathcomp.solvable.nilpotent]
lcn_bigcprod [prf, in mathcomp.solvable.nilpotent]
lcn_bigdprod [prf, in mathcomp.solvable.nilpotent]
lcn_central [prf, in mathcomp.solvable.nilpotent]
lcn_char [prf, in mathcomp.solvable.nilpotent]
lcn_cont [prf, in mathcomp.solvable.nilpotent]
lcn_cprod [prf, in mathcomp.solvable.nilpotent]
lcn_dprod [prf, in mathcomp.solvable.nilpotent]
lcn_group_set [prf, in mathcomp.solvable.nilpotent]
lcn_nil_classP [prf, in mathcomp.solvable.nilpotent]
lcn_norm [prf, in mathcomp.solvable.nilpotent]
lcn_normal [prf, in mathcomp.solvable.nilpotent]
lcn_normalS [prf, in mathcomp.solvable.nilpotent]
lcn_sub [prf, in mathcomp.solvable.nilpotent]
lcn_sub_leq [prf, in mathcomp.solvable.nilpotent]
lcn_subS [prf, in mathcomp.solvable.nilpotent]
lcnE [prf, in mathcomp.solvable.nilpotent]
lcnP [prf, in mathcomp.solvable.nilpotent]
lcnS [prf, in mathcomp.solvable.nilpotent]
lcnSn [prf, in mathcomp.solvable.nilpotent]
lcnSnS [prf, in mathcomp.solvable.nilpotent]
Lcorrect [prf, in mathcomp.solvable.burnside_app]
lcoset1 [prf, in mathcomp.finite_group.fingroup]
lcoset_eqP [prf, in mathcomp.finite_group.fingroup]
lcoset_id [prf, in mathcomp.finite_group.fingroup]
lcoset_inj [prf, in mathcomp.finite_group.fingroup]
lcoset_refl [prf, in mathcomp.finite_group.fingroup]
lcoset_sym [prf, in mathcomp.finite_group.fingroup]
lcoset_trans [prf, in mathcomp.finite_group.fingroup]
lcoset_transl [prf, in mathcomp.finite_group.fingroup]
lcosetE [prf, in mathcomp.finite_group.fingroup]
lcosetK [prf, in mathcomp.finite_group.fingroup]
lcosetKV [prf, in mathcomp.finite_group.fingroup]
lcosetM [prf, in mathcomp.finite_group.fingroup]
lcosetP [prf, in mathcomp.finite_group.fingroup]
lcosetS [prf, in mathcomp.finite_group.fingroup]
lcosetsP [prf, in mathcomp.finite_group.fingroup]
LdivJ [prf, in mathcomp.solvable.abelian]
LdivP [prf, in mathcomp.solvable.abelian]
LdivT_J [prf, in mathcomp.solvable.abelian]
le0 [prf, in mathcomp.reals.signed]
le0 [prf, in mathcomp.algebra.interval_inference]
le0_ball0 [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
le0_continuous_FTC2y [prf, in mathcomp.analysis.ftc]
le0_expectation_cdf [prf, in mathcomp.analysis.probability_theory.random_variable]
le0_fin_numE [prf, in mathcomp.reals.constructive_ereal]
le0_funenegE [prf, in mathcomp.analysis.numfun]
le0_funenegM [prf, in mathcomp.analysis.numfun]
le0_funeposE [prf, in mathcomp.analysis.numfun]
le0_funeposM [prf, in mathcomp.analysis.numfun]
le0_funrnegE [prf, in mathcomp.analysis.numfun]
le0_funrnegM [prf, in mathcomp.analysis.numfun]
le0_funrposE [prf, in mathcomp.analysis.numfun]
le0_funrposM [prf, in mathcomp.analysis.numfun]
le0_lneNy [prf, in mathcomp.analysis.exp]
le0_muleDl [prf, in mathcomp.reals.constructive_ereal]
le0_muleDr [prf, in mathcomp.reals.constructive_ereal]
le0_nondecreasing_set_cvg_integral [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg]
le0_nondecreasing_set_nonincreasing_integral [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg]
le0_sume_distrl [prf, in mathcomp.reals.constructive_ereal]
le0_sume_distrr [prf, in mathcomp.reals.constructive_ereal]
le0F [prf, in mathcomp.reals.signed]
le0F [prf, in mathcomp.algebra.interval_inference]
le0y [prf, in mathcomp.reals.constructive_ereal]
le0z_nat [prf, in mathcomp.algebra.ssrint]
le1 [prf, in mathcomp.algebra.interval_inference]
le1r_powR [prf, in mathcomp.analysis.exp]
le1r_powRZ [prf, in mathcomp.analysis.exp]
le_abse_integral [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg]
le_anti_ereal [prf, in mathcomp.reals.constructive_ereal]
le_approx [prf, in mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation]
le_atan [prf, in mathcomp.analysis.trigo]
le_ball [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
le_big_nat [prf, in mathcomp.boot.bigop]
le_big_nat_cond [prf, in mathcomp.boot.bigop]
le_big_ord [prf, in mathcomp.boot.bigop]
le_big_ord_cond [prf, in mathcomp.boot.bigop]
le_bigmax_seq [prf, in mathcomp.classical.unstable]
le_bnd_ereal [prf, in mathcomp.reals.real_interval]
le_bound_anti [prf, in mathcomp.algebra.interval]
le_bound_refl [prf, in mathcomp.algebra.interval]
le_bound_trans [prf, in mathcomp.algebra.interval]
le_caratheodory_measurable [prf, in mathcomp.analysis.measure_theory.measure_extension]
le_closed_ball [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
le_contract [prf, in mathcomp.reals.constructive_ereal]
le_down [prf, in mathcomp.reals.reals]
le_er_map [prf, in mathcomp.reals.constructive_ereal]
le_er_map_in [prf, in mathcomp.analysis.ereal]
le_ereal_ball [prf, in mathcomp.analysis.ereal]
le_ereal_inf_tmp [prf, in mathcomp.analysis.ereal]
le_ereal_sup_tmp [prf, in mathcomp.analysis.ereal]
le_ess_inf [prf, in mathcomp.analysis.ess_sup_inf]
le_ess_sup [prf, in mathcomp.analysis.ess_sup_inf]
le_esum [prf, in mathcomp.analysis.esum]
le_expand [prf, in mathcomp.reals.constructive_ereal]
le_expand_in [prf, in mathcomp.reals.constructive_ereal]
le_ext_num_itv_bound [prf, in mathcomp.reals.constructive_ereal]
le_factor [prf, in mathcomp.classical.set_interval]
le_ffix_order [prf, in mathcomp.finmap.finmap]
le_fix_order [prf, in mathcomp.finmap.finmap]
le_fix_order [prf, in mathcomp.boot.finset]
le_infimum_Nmem [prf, in mathcomp.classical.classical_sets]
le_integrable [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integrable]
le_integral [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integrable]
le_integral_abse [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg]
le_integral_comp_abse [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg]
le_irrelevance [prf, in mathcomp.boot.ssrnat]
le_limn_infD [prf, in mathcomp.analysis.sequences]
le_limn_supD [prf, in mathcomp.analysis.sequences]
le_line_path [prf, in mathcomp.classical.set_interval]
le_ln1Dx [prf, in mathcomp.analysis.exp]
le_lne1Dx [prf, in mathcomp.analysis.exp]
le_map_itv_bound_EFin [prf, in mathcomp.reals.constructive_ereal]
le_measure [prf, in mathcomp.analysis.measure_theory.measure_function]
le_measure_sintegral [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
le_mu_ext [prf, in mathcomp.analysis.measure_theory.measure_extension]
le_ninfty [prf, in mathcomp.algebra.interval]
le_normr_Rintegral [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
le_nseries [prf, in mathcomp.analysis.sequences]
le_num_itv_bound [prf, in mathcomp.algebra.interval_inference]
le_outer_measureIC [prf, in mathcomp.analysis.measure_theory.measure_extension]
le_rat0 [prf, in mathcomp.algebra.rat]
le_rat0_anti [prf, in mathcomp.algebra.rat]
le_rat0D [prf, in mathcomp.algebra.rat]
le_rat0M [prf, in mathcomp.algebra.rat]
le_rat_total [prf, in mathcomp.algebra.rat]
le_ratE [prf, in mathcomp.algebra.rat]
le_Rceil [prf, in mathcomp.reals.reals]
le_refl_ereal [prf, in mathcomp.reals.constructive_ereal]
le_Rfloor [prf, in mathcomp.reals.reals]
le_Rhull [prf, in mathcomp.analysis.normedtype_theory.normed_module]
le_Rintegral [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
le_sintegral [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
le_total_ereal [prf, in mathcomp.reals.constructive_ereal]
le_trans_ereal [prf, in mathcomp.reals.constructive_ereal]
le_variation [prf, in mathcomp.analysis.numfun]
le_wlength [prf, in mathcomp.analysis.lebesgue_stieltjes_measure]
le_wlength_itv [prf, in mathcomp.analysis.lebesgue_stieltjes_measure]
le_xsection [prf, in mathcomp.classical.classical_sets]
le_ysection [prf, in mathcomp.classical.classical_sets]
lead_coef0 [prf, in mathcomp.algebra.poly]
lead_coef1 [prf, in mathcomp.algebra.poly]
lead_coef_comp [prf, in mathcomp.algebra.poly]
lead_coef_eq0 [prf, in mathcomp.algebra.poly]
lead_coef_exp [prf, in mathcomp.algebra.poly]
lead_coef_lreg [prf, in mathcomp.algebra.poly]
lead_coef_map [prf, in mathcomp.algebra.poly]
lead_coef_map_eq [prf, in mathcomp.algebra.poly]
lead_coef_map_id0 [prf, in mathcomp.algebra.poly]
lead_coef_map_inj [prf, in mathcomp.algebra.poly]
lead_coef_Mmonic [prf, in mathcomp.algebra.poly]
lead_coef_monicM [prf, in mathcomp.algebra.poly]
lead_coef_poly [prf, in mathcomp.algebra.poly]
lead_coef_poly_XaY [prf, in mathcomp.algebra.polyXY]
lead_coef_prod [prf, in mathcomp.algebra.poly]
lead_coef_prod_XsubC [prf, in mathcomp.algebra.poly]
lead_coef_proper_mul [prf, in mathcomp.algebra.poly]
lead_coefC [prf, in mathcomp.algebra.poly]
lead_coefDl [prf, in mathcomp.algebra.poly]
lead_coefDr [prf, in mathcomp.algebra.poly]
lead_coefE [prf, in mathcomp.algebra.poly]
lead_coefM [prf, in mathcomp.algebra.poly]
lead_coefMX [prf, in mathcomp.algebra.poly]
lead_coefN [prf, in mathcomp.algebra.poly]
lead_coefX [prf, in mathcomp.algebra.poly]
lead_coefXaddC [prf, in mathcomp.algebra.poly]
lead_coefXn [prf, in mathcomp.algebra.poly]
lead_coefXnaddC [prf, in mathcomp.algebra.poly]
lead_coefXnsubC [prf, in mathcomp.algebra.poly]
lead_coefXsubC [prf, in mathcomp.algebra.poly]
lead_coefZ [prf, in mathcomp.algebra.poly]
lebesgue_density [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
lebesgue_differentiation [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
lebesgue_differentiation_continuous [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
lebesgue_integral_pmf [prf, in mathcomp.analysis.probability_theory.random_variable]
lebesgue_measure_ball [prf, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_closed_ball [prf, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_itv [prf, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_rat [prf, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_set1 [prf, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_unique [prf, in mathcomp.analysis.lebesgue_measure]
lebesgue_measureN [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg]
lebesgue_nearly_bounded [prf, in mathcomp.analysis.lebesgue_measure]
lebesgue_pt_restrict [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
lebesgue_regularity_inner [prf, in mathcomp.analysis.lebesgue_measure]
lebesgue_regularity_inner_sup [prf, in mathcomp.analysis.lebesgue_measure]
lebesgue_regularity_outer [prf, in mathcomp.analysis.lebesgue_measure]
lebesgue_stieltjes_cdf_id [prf, in mathcomp.analysis.probability_theory.random_variable]
lebesgue_stieltjes_measure_unique [prf, in mathcomp.analysis.lebesgue_stieltjes_measure]
LebesgueMeasure.finite_hlength_itv [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength0 [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength_bnd_infty [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength_finite_fin_num [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength_ge0 [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength_infty_bnd [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength_itv [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength_itv_ge0 [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength_Rhull [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength_semi_additive [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength_setT [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength_sigma_finite [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength_sigma_subadditive [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength_singleton [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.infinite_hlength_itv [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.le_hlength [prf, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.le_hlength_itv [prf, in mathcomp.analysis.lebesgue_measure]
leBRight_ltBLeft [prf, in mathcomp.algebra.interval]
leBSide [prf, in mathcomp.algebra.interval]
lee0 [prf, in mathcomp.reals.constructive_ereal]
lee01 [prf, in mathcomp.reals.constructive_ereal]
lee0_abs [prf, in mathcomp.reals.constructive_ereal]
lee0n [prf, in mathcomp.reals.constructive_ereal]
lee0N1 [prf, in mathcomp.reals.constructive_ereal]
lee1n [prf, in mathcomp.reals.constructive_ereal]
lee_abs [prf, in mathcomp.reals.constructive_ereal]
lee_abs_add [prf, in mathcomp.reals.constructive_ereal]
lee_abs_sub [prf, in mathcomp.reals.constructive_ereal]
lee_abs_sum [prf, in mathcomp.reals.constructive_ereal]
lee_addgt0Pr [prf, in mathcomp.reals.constructive_ereal]
lee_cvg_to [prf, in mathcomp.analysis.normedtype_theory.normed_module]
lee_cvgNy [prf, in mathcomp.analysis.normedtype_theory.normed_module]
lee_expeR [prf, in mathcomp.analysis.exp]
lee_fin [prf, in mathcomp.reals.constructive_ereal]
lee_fsum [prf, in mathcomp.analysis.ereal]
lee_fsum_nneg_subset [prf, in mathcomp.analysis.ereal]
lee_lim [prf, in mathcomp.analysis.normedtype_theory.normed_module]
lee_lne [prf, in mathcomp.analysis.exp]
lee_ltD [prf, in mathcomp.reals.constructive_ereal]
lee_mul01Pr [prf, in mathcomp.reals.constructive_ereal]
lee_ndivlMl [prf, in mathcomp.reals.constructive_ereal]
lee_ndivlMr [prf, in mathcomp.reals.constructive_ereal]
lee_ndivrMl [prf, in mathcomp.reals.constructive_ereal]
lee_ndivrMr [prf, in mathcomp.reals.constructive_ereal]
lee_nemull [prf, in mathcomp.reals.constructive_ereal]
lee_nemulr [prf, in mathcomp.reals.constructive_ereal]
lee_nneseries [prf, in mathcomp.analysis.sequences]
lee_npeseries [prf, in mathcomp.analysis.sequences]
lee_paddl [prf, in mathcomp.reals.constructive_ereal]
lee_paddr [prf, in mathcomp.reals.constructive_ereal]
lee_pdivlMl [prf, in mathcomp.reals.constructive_ereal]
lee_pdivlMr [prf, in mathcomp.reals.constructive_ereal]
lee_pdivrMl [prf, in mathcomp.reals.constructive_ereal]
lee_pdivrMr [prf, in mathcomp.reals.constructive_ereal]
lee_pemull [prf, in mathcomp.reals.constructive_ereal]
lee_pemulr [prf, in mathcomp.reals.constructive_ereal]
lee_pmul [prf, in mathcomp.reals.constructive_ereal]
lee_pmul2l [prf, in mathcomp.reals.constructive_ereal]
lee_pmul2r [prf, in mathcomp.reals.constructive_ereal]
lee_pV2 [prf, in mathcomp.reals.constructive_ereal]
lee_restrict [prf, in mathcomp.analysis.numfun]
lee_sqr [prf, in mathcomp.reals.constructive_ereal]
lee_sqrE [prf, in mathcomp.reals.constructive_ereal]
lee_sqrt [prf, in mathcomp.reals.constructive_ereal]
lee_subel_addl [prf, in mathcomp.reals.constructive_ereal]
lee_subel_addr [prf, in mathcomp.reals.constructive_ereal]
lee_suber_addl [prf, in mathcomp.reals.constructive_ereal]
lee_suber_addr [prf, in mathcomp.reals.constructive_ereal]
lee_subgt0Pr [prf, in mathcomp.reals.constructive_ereal]
lee_sum [prf, in mathcomp.reals.constructive_ereal]
lee_sum_fset_lim [prf, in mathcomp.analysis.esum]
lee_sum_fset_nat [prf, in mathcomp.analysis.esum]
lee_sum_nneg [prf, in mathcomp.reals.constructive_ereal]
lee_sum_nneg_natl [prf, in mathcomp.reals.constructive_ereal]
lee_sum_nneg_natr [prf, in mathcomp.reals.constructive_ereal]
lee_sum_nneg_ord [prf, in mathcomp.reals.constructive_ereal]
lee_sum_nneg_subfset [prf, in mathcomp.reals.constructive_ereal]
lee_sum_nneg_subset [prf, in mathcomp.reals.constructive_ereal]
lee_sum_npos [prf, in mathcomp.reals.constructive_ereal]
lee_sum_npos_natl [prf, in mathcomp.reals.constructive_ereal]
lee_sum_npos_natr [prf, in mathcomp.reals.constructive_ereal]
lee_sum_npos_ord [prf, in mathcomp.reals.constructive_ereal]
lee_sum_npos_subfset [prf, in mathcomp.reals.constructive_ereal]
lee_sum_npos_subset [prf, in mathcomp.reals.constructive_ereal]
lee_tofin [prf, in mathcomp.reals.constructive_ereal]
lee_wpmul2l [prf, in mathcomp.reals.constructive_ereal]
lee_wpmul2r [prf, in mathcomp.reals.constructive_ereal]
leeB [prf, in mathcomp.reals.constructive_ereal]
leEbig_lexi_order [prf, in mathcomp.classical.classical_orders]
leeBlDl [prf, in mathcomp.reals.constructive_ereal]
leeBlDr [prf, in mathcomp.reals.constructive_ereal]
leeBrDl [prf, in mathcomp.reals.constructive_ereal]
leeBrDr [prf, in mathcomp.reals.constructive_ereal]
leeD [prf, in mathcomp.reals.constructive_ereal]
leeD2l [prf, in mathcomp.reals.constructive_ereal]
leeD2lE [prf, in mathcomp.reals.constructive_ereal]
leeD2r [prf, in mathcomp.reals.constructive_ereal]
leeD2rE [prf, in mathcomp.reals.constructive_ereal]
leeDl [prf, in mathcomp.reals.constructive_ereal]
leeDr [prf, in mathcomp.reals.constructive_ereal]
leEereal [prf, in mathcomp.reals.constructive_ereal]
leeN10 [prf, in mathcomp.reals.constructive_ereal]
leeN2 [prf, in mathcomp.reals.constructive_ereal]
leeNl [prf, in mathcomp.reals.constructive_ereal]
leeNr [prf, in mathcomp.reals.constructive_ereal]
leeNy_eq [prf, in mathcomp.reals.constructive_ereal]
leey [prf, in mathcomp.reals.constructive_ereal]
lef_at [prf, in mathcomp.analysis.sequences]
lefP [prf, in mathcomp.classical.boolp]
left_arc [prf, in mathcomp.boot.path]
left_bounded_interior [prf, in mathcomp.analysis.topology_theory.num_topology]
left_right_continuousP [prf, in mathcomp.analysis.topology_theory.num_topology]
left_trans [prf, in mathcomp.boot.generic_quotient]
lem [prf, in mathcomp.classical.boolp]
leNy0 [prf, in mathcomp.reals.constructive_ereal]
leNye [prf, in mathcomp.reals.constructive_ereal]
leNz_nat [prf, in mathcomp.algebra.ssrint]
leP [prf, in mathcomp.boot.ssrnat]
leq0n [prf, in mathcomp.boot.ssrnat]
leq_add [prf, in mathcomp.boot.ssrnat]
leq_add2l [prf, in mathcomp.boot.ssrnat]
leq_add2r [prf, in mathcomp.boot.ssrnat]
leq_addl [prf, in mathcomp.boot.ssrnat]
leq_addr [prf, in mathcomp.boot.ssrnat]
leq_b1 [prf, in mathcomp.boot.ssrnat]
leq_bigmax [prf, in mathcomp.boot.bigop]
leq_bigmax_cond [prf, in mathcomp.boot.bigop]
leq_bigmax_seq [prf, in mathcomp.boot.bigop]
leq_bin2l [prf, in mathcomp.boot.binomial]
leq_bump [prf, in mathcomp.boot.fintype]
leq_bump2 [prf, in mathcomp.boot.fintype]
leq_card [prf, in mathcomp.boot.fintype]
leq_card_cover [prf, in mathcomp.boot.finset]
leq_card_fcover [prf, in mathcomp.finmap.finmap]
leq_card_fset_set [prf, in mathcomp.classical.cardinality]
leq_card_fsetU [prf, in mathcomp.finmap.finmap]
leq_card_in [prf, in mathcomp.boot.fintype]
leq_card_setU [prf, in mathcomp.boot.finset]
leq_count_mask [prf, in mathcomp.boot.seq]
leq_count_subseq [prf, in mathcomp.boot.seq]
leq_dim_orthov1 [prf, in mathcomp.algebra.sesquilinear]
leq_div [prf, in mathcomp.boot.div]
leq_div2l [prf, in mathcomp.boot.div]
leq_div2r [prf, in mathcomp.boot.div]
leq_divDl [prf, in mathcomp.boot.div]
leq_divLR [prf, in mathcomp.boot.div]
leq_divM [prf, in mathcomp.boot.div]
leq_divRL [prf, in mathcomp.boot.div]
leq_double [prf, in mathcomp.boot.ssrnat]
leq_eqVlt [prf, in mathcomp.boot.ssrnat]
leq_exp2l [prf, in mathcomp.boot.ssrnat]
leq_exp2r [prf, in mathcomp.boot.ssrnat]
leq_fact [prf, in mathcomp.boot.ssrnat]
leq_fact2 [prf, in mathcomp.classical.unstable]
leq_geP [prf, in mathcomp.boot.ssrnat]
leq_gtF [prf, in mathcomp.boot.ssrnat]
leq_gtP [prf, in mathcomp.boot.ssrnat]
leq_half_double [prf, in mathcomp.boot.ssrnat]
leq_homg [prf, in mathcomp.finite_group.morphism]
leq_image_card [prf, in mathcomp.boot.fintype]
leq_imfset_card [prf, in mathcomp.finmap.finmap]
leq_imset_card [prf, in mathcomp.boot.finset]
leq_leP [prf, in mathcomp.boot.ssrnat]
leq_ltn_expn [prf, in mathcomp.classical.unstable]
leq_ltn_trans [prf, in mathcomp.boot.ssrnat]
leq_ltP [prf, in mathcomp.boot.ssrnat]
leq_max [prf, in mathcomp.boot.ssrnat]
leq_maxl [prf, in mathcomp.boot.ssrnat]
leq_maxr [prf, in mathcomp.boot.ssrnat]
leq_min [prf, in mathcomp.boot.ssrnat]
leq_mod [prf, in mathcomp.boot.div]
leq_mono [prf, in mathcomp.boot.ssrnat]
leq_mono_in [prf, in mathcomp.boot.ssrnat]
leq_morphim [prf, in mathcomp.finite_group.morphism]
leq_Mprod_prodD [prf, in mathcomp.classical.unstable]
leq_mul [prf, in mathcomp.boot.ssrnat]
leq_mul2l [prf, in mathcomp.boot.ssrnat]
leq_mul2r [prf, in mathcomp.boot.ssrnat]
leq_nmono [prf, in mathcomp.boot.ssrnat]
leq_nmono_in [prf, in mathcomp.boot.ssrnat]
leq_ord [prf, in mathcomp.boot.fintype]
leq_pexp2l [prf, in mathcomp.boot.ssrnat]
leq_pfact [prf, in mathcomp.boot.ssrnat]
leq_pmul2l [prf, in mathcomp.boot.ssrnat]
leq_pmul2r [prf, in mathcomp.boot.ssrnat]
leq_pmull [prf, in mathcomp.boot.ssrnat]
leq_pmulr [prf, in mathcomp.boot.ssrnat]
leq_pred [prf, in mathcomp.boot.ssrnat]
leq_prod [prf, in mathcomp.boot.bigop]
leq_psubCr [prf, in mathcomp.boot.ssrnat]
leq_psubRL [prf, in mathcomp.boot.ssrnat]
leq_quotient [prf, in mathcomp.finite_group.quotient]
leq_rot_add [prf, in mathcomp.boot.seq]
leq_Sdouble [prf, in mathcomp.boot.ssrnat]
leq_size_uniq [prf, in mathcomp.boot.seq]
leq_sizeP [prf, in mathcomp.algebra.poly]
leq_sqr [prf, in mathcomp.boot.ssrnat]
leq_sub [prf, in mathcomp.boot.ssrnat]
leq_sub2l [prf, in mathcomp.boot.ssrnat]
leq_sub2lE [prf, in mathcomp.boot.ssrnat]
leq_sub2r [prf, in mathcomp.boot.ssrnat]
leq_sub2rE [prf, in mathcomp.boot.ssrnat]
leq_subCl [prf, in mathcomp.boot.ssrnat]
leq_subCr [prf, in mathcomp.boot.ssrnat]
leq_subLR [prf, in mathcomp.boot.ssrnat]
leq_subr [prf, in mathcomp.boot.ssrnat]
leq_subRL [prf, in mathcomp.boot.ssrnat]
leq_subrR [prf, in mathcomp.boot.ssrnat]
leq_sum [prf, in mathcomp.boot.bigop]
leq_total [prf, in mathcomp.boot.ssrnat]
leq_trans [prf, in mathcomp.boot.ssrnat]
leq_trunc_log [prf, in mathcomp.boot.prime]
leq_uniq_count [prf, in mathcomp.boot.seq]
leq_uniq_countP [prf, in mathcomp.boot.seq]
leq_up_log [prf, in mathcomp.boot.prime]
leq_uphalf_double [prf, in mathcomp.boot.ssrnat]
leqDmod [prf, in mathcomp.boot.div]
leqif_add [prf, in mathcomp.boot.ssrnat]
leqif_dim_orthov1 [prf, in mathcomp.algebra.sesquilinear]
leqif_dim_orthov1_full [prf, in mathcomp.algebra.sesquilinear]
leqif_eq [prf, in mathcomp.boot.ssrnat]
leqif_geq [prf, in mathcomp.boot.ssrnat]
leqif_mul [prf, in mathcomp.boot.ssrnat]
leqif_refl [prf, in mathcomp.boot.ssrnat]
leqif_sum [prf, in mathcomp.boot.bigop]
leqif_trans [prf, in mathcomp.boot.ssrnat]
leqifP [prf, in mathcomp.boot.ssrnat]
leqn0 [prf, in mathcomp.boot.ssrnat]
leqNgt [prf, in mathcomp.boot.ssrnat]
leqnn [prf, in mathcomp.boot.ssrnat]
leqnSn [prf, in mathcomp.boot.ssrnat]
leqP [prf, in mathcomp.boot.ssrnat]
leqSpred [prf, in mathcomp.boot.ssrnat]
leqVgt [prf, in mathcomp.boot.ssrnat]
leqW [prf, in mathcomp.boot.ssrnat]
leqW_mono [prf, in mathcomp.boot.ssrnat]
leqW_mono_in [prf, in mathcomp.boot.ssrnat]
leqW_nmono [prf, in mathcomp.boot.ssrnat]
leqW_nmono_in [prf, in mathcomp.boot.ssrnat]
ler0_derive1_le [prf, in mathcomp.analysis.derive]
ler0_derive1_le_cc [prf, in mathcomp.analysis.derive]
ler0_derive1_le_co [prf, in mathcomp.analysis.derive]
ler0_derive1_le_oc [prf, in mathcomp.analysis.derive]
ler0_derive1_le_oo [prf, in mathcomp.analysis.derive]
ler0_derive1_nincr [prf, in mathcomp.analysis.derive]
ler0_derive1_nincrNy [prf, in mathcomp.analysis.derive]
ler0_derive1_nincry [prf, in mathcomp.analysis.derive]
ler0q [prf, in mathcomp.algebra.rat]
ler0z [prf, in mathcomp.algebra.ssrint]
ler1_powR [prf, in mathcomp.analysis.exp]
ler1z [prf, in mathcomp.algebra.ssrint]
ler_cvg_to [prf, in mathcomp.analysis.normedtype_theory.normed_module]
ler_cvgNy [prf, in mathcomp.analysis.normedtype_theory.normed_module]
ler_expR [prf, in mathcomp.analysis.exp]
ler_eXz2l [prf, in mathcomp.algebra.ssrint]
ler_gtP [prf, in mathcomp.classical.unstable]
ler_int [prf, in mathcomp.algebra.ssrint]
ler_lim [prf, in mathcomp.analysis.normedtype_theory.normed_module]
ler_ln [prf, in mathcomp.analysis.exp]
ler_LnormD [prf, in mathcomp.analysis.hoelder]
ler_ltP [prf, in mathcomp.classical.unstable]
ler_mx_norm_add [prf, in mathcomp.analysis.normedtype_theory.matrix_normedtype]
ler_niXz2l [prf, in mathcomp.algebra.ssrint]
ler_nMz2l [prf, in mathcomp.algebra.ssrint]
ler_nMz2r [prf, in mathcomp.algebra.ssrint]
ler_nXz2r [prf, in mathcomp.algebra.ssrint]
ler_piXz2l [prf, in mathcomp.algebra.ssrint]
ler_pMz2l [prf, in mathcomp.algebra.ssrint]
ler_pMz2r [prf, in mathcomp.algebra.ssrint]
ler_powR [prf, in mathcomp.analysis.exp]
ler_pXz2r [prf, in mathcomp.algebra.ssrint]
ler_rat [prf, in mathcomp.algebra.rat]
ler_restrict [prf, in mathcomp.analysis.numfun]
ler_weXz2l [prf, in mathcomp.algebra.ssrint]
ler_wneXz2l [prf, in mathcomp.algebra.ssrint]
ler_wniXz2l [prf, in mathcomp.algebra.ssrint]
ler_wnMz2l [prf, in mathcomp.algebra.ssrint]
ler_wnMz2r [prf, in mathcomp.algebra.ssrint]
ler_wnXz2r [prf, in mathcomp.algebra.ssrint]
ler_wpeXz2l [prf, in mathcomp.algebra.ssrint]
ler_wpiXz2l [prf, in mathcomp.algebra.ssrint]
ler_wpMz2l [prf, in mathcomp.algebra.ssrint]
ler_wpMz2r [prf, in mathcomp.algebra.ssrint]
ler_wpXz2r [prf, in mathcomp.algebra.ssrint]
lerB_DLnorm [prf, in mathcomp.analysis.hoelder]
lerB_LnormD [prf, in mathcomp.analysis.hoelder]
lerq0 [prf, in mathcomp.algebra.rat]
lerz0 [prf, in mathcomp.algebra.ssrint]
lerz1 [prf, in mathcomp.algebra.ssrint]
leW_factor [prf, in mathcomp.classical.set_interval]
leW_line_path [prf, in mathcomp.classical.set_interval]
leye_eq [prf, in mathcomp.reals.constructive_ereal]
lez0_abs [prf, in mathcomp.algebra.ssrint]
lez0_nat [prf, in mathcomp.algebra.ssrint]
lez1D [prf, in mathcomp.algebra.ssrint]
lez_abs [prf, in mathcomp.algebra.ssrint]
lez_abs2 [prf, in mathcomp.classical.unstable]
lez_div [prf, in mathcomp.algebra.intdiv]
lez_divLR [prf, in mathcomp.algebra.intdiv]
lez_divRL [prf, in mathcomp.algebra.intdiv]
lez_floor [prf, in mathcomp.algebra.intdiv]
lez_nat [prf, in mathcomp.algebra.ssrint]
lez_pdiv2r [prf, in mathcomp.algebra.intdiv]
lezD1 [prf, in mathcomp.algebra.ssrint]
lezN_nat [prf, in mathcomp.algebra.ssrint]
Lfun1_integrable [prf, in mathcomp.analysis.hoelder]
lfun1_neq0 [prf, in mathcomp.algebra.vector]
lfun1_poly [prf, in mathcomp.field.falgebra]
Lfun2_integrable_sqr [prf, in mathcomp.analysis.hoelder]
Lfun2_mul_Lfun1 [prf, in mathcomp.analysis.hoelder]
lfun_add0 [prf, in mathcomp.algebra.vector]
lfun_addA [prf, in mathcomp.algebra.vector]
lfun_addC [prf, in mathcomp.algebra.vector]
lfun_addN [prf, in mathcomp.algebra.vector]
Lfun_addr_closed [prf, in mathcomp.analysis.hoelder]
Lfun_cst [prf, in mathcomp.analysis.hoelder]
lfun_img_key [prf, in mathcomp.algebra.vector]
Lfun_integrable [prf, in mathcomp.analysis.hoelder]
lfun_is_semilinear [prf, in mathcomp.algebra.vector]
lfun_key [prf, in mathcomp.algebra.vector]
Lfun_norm [prf, in mathcomp.analysis.hoelder]
Lfun_oppr_closed [prf, in mathcomp.analysis.hoelder]
Lfun_rect [prf, in mathcomp.analysis.hoelder]
Lfun_scale [prf, in mathcomp.analysis.hoelder]
lfun_scale0 [prf, in mathcomp.algebra.vector]
lfun_scale1 [prf, in mathcomp.algebra.vector]
lfun_scaleA [prf, in mathcomp.algebra.vector]
lfun_scaleDl [prf, in mathcomp.algebra.vector]
lfun_scaleDr [prf, in mathcomp.algebra.vector]
Lfun_submod_closed [prf, in mathcomp.analysis.hoelder]
Lfun_subset [prf, in mathcomp.analysis.hoelder]
Lfun_subset12 [prf, in mathcomp.analysis.hoelder]
Lfun_valP [prf, in mathcomp.analysis.hoelder]
lfun_vect_iso [prf, in mathcomp.algebra.vector]
lfunE [prf, in mathcomp.algebra.vector]
LfuneqP [prf, in mathcomp.analysis.hoelder]
LfunP [prf, in mathcomp.analysis.hoelder]
lfunP [prf, in mathcomp.algebra.vector]
lfunPn [prf, in mathcomp.algebra.vector]
lhopital [prf, in mathcomp.analysis.realfun]
lhopital_at_left [prf, in mathcomp.analysis.realfun]
lhopital_at_right [prf, in mathcomp.analysis.realfun]
lift0 [prf, in mathcomp.boot.fintype]
lift0_mx_is_perm [prf, in mathcomp.algebra.matrix]
lift0_mx_perm [prf, in mathcomp.algebra.matrix]
lift0_perm0 [prf, in mathcomp.finite_group.perm]
lift0_perm_eq0 [prf, in mathcomp.finite_group.perm]
lift0_perm_lift [prf, in mathcomp.finite_group.perm]
lift0_permK [prf, in mathcomp.finite_group.perm]
lift_eqF [prf, in mathcomp.boot.fintype]
lift_inj [prf, in mathcomp.boot.fintype]
lift_max [prf, in mathcomp.boot.fintype]
lift_perm1 [prf, in mathcomp.finite_group.perm]
lift_perm_id [prf, in mathcomp.finite_group.perm]
lift_perm_lift [prf, in mathcomp.finite_group.perm]
lift_permK [prf, in mathcomp.finite_group.perm]
lift_permM [prf, in mathcomp.finite_group.perm]
lift_permV [prf, in mathcomp.finite_group.perm]
liftK [prf, in mathcomp.boot.fintype]
lim0g [prf, in mathcomp.algebra.vector]
lim1g [prf, in mathcomp.algebra.vector]
lim_cst [prf, in mathcomp.analysis.topology_theory.separation_axioms]
lim_cvg_to_0_linear [prf, in mathcomp.analysis.sequences]
lim_id [prf, in mathcomp.analysis.topology_theory.separation_axioms]
lim_lime_inf [prf, in mathcomp.analysis.realfun]
lim_lime_inf' [prf, in mathcomp.analysis.realfun]
lim_lime_sup [prf, in mathcomp.analysis.realfun]
lim_lime_sup' [prf, in mathcomp.analysis.realfun]
lim_max_approxRN_seq.epsRN_ex [prf, in mathcomp.analysis.charge]
lim_max_approxRN_seq.fRN_ge0 [prf, in mathcomp.analysis.charge]
lim_max_approxRN_seq.int_fRN_lty [prf, in mathcomp.analysis.charge]
lim_max_approxRN_seq.int_fRN_ub [prf, in mathcomp.analysis.charge]
lim_max_approxRN_seq.int_fRNE [prf, in mathcomp.analysis.charge]
lim_max_approxRN_seq.measurable_fun_fRN [prf, in mathcomp.analysis.charge]
lim_mkord [prf, in mathcomp.analysis.sequences]
lim_near_cst [prf, in mathcomp.analysis.topology_theory.separation_axioms]
lim_nnesum [prf, in mathcomp.analysis.normedtype_theory.normed_module]
lim_norm [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
lim_series_le [prf, in mathcomp.analysis.sequences]
lim_series_norm [prf, in mathcomp.analysis.sequences]
lim_seriesB [prf, in mathcomp.analysis.sequences]
lim_seriesD [prf, in mathcomp.analysis.sequences]
lim_seriesN [prf, in mathcomp.analysis.sequences]
lim_seriesZ [prf, in mathcomp.analysis.sequences]
lim_sup_davg_ge0 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
lim_sup_davg_le [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
lim_sup_davgB [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
lim_sup_davgT_HL_maximal [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
lim_sup_set_cvg [prf, in mathcomp.analysis.measure_theory.measure_function]
lim_sup_set_cvg0 [prf, in mathcomp.analysis.measure_theory.measure_function]
lim_sup_set_ub [prf, in mathcomp.analysis.measure_theory.measure_function]
limB [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
limD [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
lime_ge [prf, in mathcomp.analysis.normedtype_theory.ereal_normedtype]
lime_inf_ge0 [prf, in mathcomp.analysis.realfun]
lime_inf_lim [prf, in mathcomp.analysis.realfun]
lime_inf_sup [prf, in mathcomp.analysis.realfun]
lime_infE [prf, in mathcomp.analysis.realfun]
lime_infN [prf, in mathcomp.analysis.realfun]
lime_infP [prf, in mathcomp.analysis.realfun]
lime_le [prf, in mathcomp.analysis.normedtype_theory.ereal_normedtype]
lime_sup_inf_at_left [prf, in mathcomp.analysis.realfun]
lime_sup_inf_at_right [prf, in mathcomp.analysis.realfun]
lime_sup_le [prf, in mathcomp.analysis.realfun]
lime_sup_lim [prf, in mathcomp.analysis.realfun]
lime_supD [prf, in mathcomp.analysis.realfun]
lime_supE [prf, in mathcomp.analysis.realfun]
lime_supN [prf, in mathcomp.analysis.realfun]
lime_supP [prf, in mathcomp.analysis.realfun]
limeD [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limeM [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limeMl [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limeMr [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limeN [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limf_einfE [prf, in mathcomp.analysis.normedtype_theory.ereal_normedtype]
limf_einfN [prf, in mathcomp.analysis.normedtype_theory.ereal_normedtype]
limf_esup_dnbhsN [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limf_esup_ge0 [prf, in mathcomp.analysis.normedtype_theory.ereal_normedtype]
limf_esupE [prf, in mathcomp.analysis.normedtype_theory.ereal_normedtype]
limf_esupN [prf, in mathcomp.analysis.normedtype_theory.ereal_normedtype]
limg0 [prf, in mathcomp.algebra.vector]
limg_amulr [prf, in mathcomp.field.falgebra]
limg_basis_of [prf, in mathcomp.algebra.vector]
limg_bigcap [prf, in mathcomp.algebra.vector]
limg_cap [prf, in mathcomp.algebra.vector]
limg_comp [prf, in mathcomp.algebra.vector]
limg_dim_eq [prf, in mathcomp.algebra.vector]
limg_gal [prf, in mathcomp.field.galois]
limg_ker0 [prf, in mathcomp.algebra.vector]
limg_ker_compl [prf, in mathcomp.algebra.vector]
limg_ker_dim [prf, in mathcomp.algebra.vector]
limg_lfunVK [prf, in mathcomp.algebra.vector]
limg_line [prf, in mathcomp.algebra.vector]
limg_proj [prf, in mathcomp.algebra.vector]
limg_span [prf, in mathcomp.algebra.vector]
limg_sum [prf, in mathcomp.algebra.vector]
limgD [prf, in mathcomp.algebra.vector]
limgS [prf, in mathcomp.algebra.vector]
limit_point_closed [prf, in mathcomp.analysis.topology_theory.separation_axioms]
limit_point_cluster_eventually [prf, in mathcomp.analysis.sequences]
limit_point_infinite_setP [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limit_point_setD [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limit_pointEnbhs [prf, in mathcomp.analysis.topology_theory.topology_structure]
limit_pointEonbhs [prf, in mathcomp.analysis.topology_theory.topology_structure]
limit_pointP [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limM [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limN [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
limn_einf_lim [prf, in mathcomp.analysis.sequences]
limn_einf_shift [prf, in mathcomp.analysis.sequences]
limn_einf_sup [prf, in mathcomp.analysis.sequences]
limn_einfN [prf, in mathcomp.analysis.sequences]
limn_esup_le_cvg [prf, in mathcomp.analysis.sequences]
limn_esup_lim [prf, in mathcomp.analysis.sequences]
limn_esupN [prf, in mathcomp.analysis.sequences]
limn_inf_sup [prf, in mathcomp.analysis.sequences]
limn_infD [prf, in mathcomp.analysis.sequences]
limn_infE [prf, in mathcomp.analysis.sequences]
limn_infN [prf, in mathcomp.analysis.sequences]
limn_supD [prf, in mathcomp.analysis.sequences]
limn_supE [prf, in mathcomp.analysis.sequences]
limr_ge [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limr_le [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limV [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limZ [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limZl_tmp [prf, in mathcomp.analysis.normedtype_theory.normed_module]
limZr_tmp [prf, in mathcomp.analysis.normedtype_theory.normed_module]
lin1_mx_key [prf, in mathcomp.algebra.matrix]
lin_mul_row_is_linear [prf, in mathcomp.algebra.matrix]
lin_mul_row_is_semilinear [prf, in mathcomp.algebra.matrix]
lin_mulmx_is_linear [prf, in mathcomp.algebra.matrix]
lin_mulmx_is_semilinear [prf, in mathcomp.algebra.matrix]
lin_mulmxr_is_linear [prf, in mathcomp.algebra.matrix]
lin_mulmxr_is_semilinear [prf, in mathcomp.algebra.matrix]
line_path0 [prf, in mathcomp.classical.set_interval]
line_path1 [prf, in mathcomp.classical.set_interval]
line_path10 [prf, in mathcomp.classical.set_interval]
line_path_bij [prf, in mathcomp.classical.set_interval]
line_path_flat [prf, in mathcomp.classical.set_interval]
line_path_id [prf, in mathcomp.classical.set_interval]
line_path_inj [prf, in mathcomp.classical.set_interval]
line_path_itv_bij [prf, in mathcomp.classical.set_interval]
line_path_sym [prf, in mathcomp.classical.set_interval]
line_pathEl [prf, in mathcomp.classical.set_interval]
line_pathEr [prf, in mathcomp.classical.set_interval]
line_pathK [prf, in mathcomp.classical.set_interval]
linear0l [prf, in mathcomp.algebra.sesquilinear]
linear0r [prf, in mathcomp.algebra.sesquilinear]
linear_bounded_continuous [prf, in mathcomp.analysis.normedtype_theory.normed_module]
linear_boundedP [prf, in mathcomp.analysis.normedtype_theory.normed_module]
linear_continuous [prf, in mathcomp.analysis.landau]
linear_differentiable [prf, in mathcomp.analysis.derive]
linear_eqO [prf, in mathcomp.analysis.derive]
linear_for_continuous [prf, in mathcomp.analysis.landau]
linear_for_mul_continuous [prf, in mathcomp.analysis.landau]
linear_lipschitz [prf, in mathcomp.analysis.derive]
linear_of_free [prf, in mathcomp.algebra.vector]
linear_sumlz [prf, in mathcomp.algebra.sesquilinear]
linear_sumr [prf, in mathcomp.algebra.sesquilinear]
linearBl [prf, in mathcomp.algebra.sesquilinear]
linearBr [prf, in mathcomp.algebra.sesquilinear]
linearDl [prf, in mathcomp.algebra.sesquilinear]
linearDr [prf, in mathcomp.algebra.sesquilinear]
linearMn [prf, in mathcomp.algebra.ssrint]
linearMnl [prf, in mathcomp.algebra.sesquilinear]
linearMNnl [prf, in mathcomp.algebra.sesquilinear]
linearMNnr [prf, in mathcomp.algebra.sesquilinear]
linearMnr [prf, in mathcomp.algebra.sesquilinear]
linearNl [prf, in mathcomp.algebra.sesquilinear]
linearNr [prf, in mathcomp.algebra.sesquilinear]
linearPl [prf, in mathcomp.algebra.sesquilinear]
linearPr [prf, in mathcomp.algebra.sesquilinear]
linearZl [prf, in mathcomp.algebra.sesquilinear]
linearZl_LR [prf, in mathcomp.algebra.sesquilinear]
linearZlr [prf, in mathcomp.algebra.sesquilinear]
linearZr [prf, in mathcomp.algebra.sesquilinear]
linearZr_LR [prf, in mathcomp.algebra.sesquilinear]
linearZrl [prf, in mathcomp.algebra.sesquilinear]
linfun_is_ahom [prf, in mathcomp.field.falgebra]
lipschitz_id [prf, in mathcomp.analysis.normedtype_theory.normed_module]
lipschitz_locally [prf, in mathcomp.analysis.normedtype_theory.normed_module]
lipschitz_set0 [prf, in mathcomp.analysis.normedtype_theory.normed_module]
lipschitz_set1 [prf, in mathcomp.analysis.normedtype_theory.normed_module]
littleo [prf, in mathcomp.analysis.landau]
littleo_bigO_eqo [prf, in mathcomp.analysis.landau]
littleo_center0 [prf, in mathcomp.analysis.derive]
littleo_class [prf, in mathcomp.analysis.landau]
littleo_eqO [prf, in mathcomp.analysis.landau]
littleo_eqo [prf, in mathcomp.analysis.landau]
littleo_lim0 [prf, in mathcomp.analysis.derive]
littleo_linear0 [prf, in mathcomp.analysis.derive]
littleo_littleo [prf, in mathcomp.analysis.landau]
littleoE [prf, in mathcomp.analysis.landau]
littleoE0 [prf, in mathcomp.analysis.landau]
littleoP [prf, in mathcomp.analysis.landau]
lker0_amull [prf, in mathcomp.field.falgebra]
lker0_amulr [prf, in mathcomp.field.falgebra]
lker0_compfK [prf, in mathcomp.algebra.vector]
lker0_compfV [prf, in mathcomp.algebra.vector]
lker0_compfVK [prf, in mathcomp.algebra.vector]
lker0_compKf [prf, in mathcomp.algebra.vector]
lker0_compVf [prf, in mathcomp.algebra.vector]
lker0_compVKf [prf, in mathcomp.algebra.vector]
lker0_img_cap [prf, in mathcomp.algebra.vector]
lker0_lfunK [prf, in mathcomp.algebra.vector]
lker0_lfunVK [prf, in mathcomp.algebra.vector]
lker0_limgf [prf, in mathcomp.algebra.vector]
lker0P [prf, in mathcomp.algebra.vector]
lker_proj [prf, in mathcomp.algebra.vector]
lkerE [prf, in mathcomp.algebra.vector]
ln0 [prf, in mathcomp.analysis.exp]
ln1 [prf, in mathcomp.analysis.exp]
ln_div [prf, in mathcomp.analysis.exp]
ln_eq0 [prf, in mathcomp.analysis.exp]
ln_ge0 [prf, in mathcomp.analysis.exp]
ln_gt0 [prf, in mathcomp.analysis.exp]
ln_inj [prf, in mathcomp.analysis.exp]
ln_le0 [prf, in mathcomp.analysis.exp]
ln_lt0 [prf, in mathcomp.analysis.exp]
ln_powR [prf, in mathcomp.analysis.exp]
ln_sublinear [prf, in mathcomp.analysis.exp]
lne1 [prf, in mathcomp.analysis.exp]
lne_div [prf, in mathcomp.analysis.exp]
lne_EFin [prf, in mathcomp.analysis.exp]
lne_eq0 [prf, in mathcomp.analysis.exp]
lne_ge0 [prf, in mathcomp.analysis.exp]
lne_gt0 [prf, in mathcomp.analysis.exp]
lne_inj [prf, in mathcomp.analysis.exp]
lne_le0 [prf, in mathcomp.analysis.exp]
lne_lt0 [prf, in mathcomp.analysis.exp]
lne_sublinear [prf, in mathcomp.analysis.exp]
lneK [prf, in mathcomp.analysis.exp]
lneK_eq [prf, in mathcomp.analysis.exp]
lneM [prf, in mathcomp.analysis.exp]
lneV [prf, in mathcomp.analysis.exp]
lneXn [prf, in mathcomp.analysis.exp]
lnK [prf, in mathcomp.analysis.exp]
lnK_eq [prf, in mathcomp.analysis.exp]
lnM [prf, in mathcomp.analysis.exp]
lnNy [prf, in mathcomp.analysis.exp]
Lnorm0 [prf, in mathcomp.analysis.hoelder]
Lnorm1 [prf, in mathcomp.analysis.hoelder]
Lnorm_abse [prf, in mathcomp.analysis.hoelder]
Lnorm_counting [prf, in mathcomp.analysis.hoelder]
Lnorm_cst1 [prf, in mathcomp.analysis.hoelder]
Lnorm_eq0_eq0 [prf, in mathcomp.analysis.hoelder]
Lnorm_ge0 [prf, in mathcomp.analysis.hoelder]
Lnormr_natmul [prf, in mathcomp.analysis.hoelder]
LnormrN [prf, in mathcomp.analysis.hoelder]
LnormZ [prf, in mathcomp.analysis.hoelder]
lnV [prf, in mathcomp.analysis.exp]
lnXn [prf, in mathcomp.analysis.exp]
locally_compact_completely_regular [prf, in mathcomp.analysis.normedtype_theory.urysohn]
locally_compactR [prf, in mathcomp.analysis.normedtype_theory.normed_module]
locally_integrable_indic [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
locally_integrableB [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
locally_integrableD [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
locally_integrableN [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
locally_integrableS [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
logn0 [prf, in mathcomp.boot.prime]
logn1 [prf, in mathcomp.boot.prime]
logn_card_GL_p [prf, in mathcomp.algebra.mxalgebra]
logn_coprime [prf, in mathcomp.boot.prime]
logn_count_dvd [prf, in mathcomp.boot.prime]
logn_div [prf, in mathcomp.boot.prime]
logn_fact [prf, in mathcomp.boot.binomial]
logn_Gauss [prf, in mathcomp.boot.prime]
logn_gcd [prf, in mathcomp.boot.prime]
logn_gt0 [prf, in mathcomp.boot.prime]
logn_lcm [prf, in mathcomp.boot.prime]
logn_le_p_rank [prf, in mathcomp.solvable.abelian]
logn_morphim [prf, in mathcomp.finite_group.quotient]
logn_part [prf, in mathcomp.boot.prime]
logn_prime [prf, in mathcomp.boot.prime]
logn_quotient [prf, in mathcomp.solvable.abelian]
logn_quotient_cent_cyclic_pgroup [prf, in mathcomp.solvable.pgroup]
lognE [prf, in mathcomp.boot.prime]
lognM [prf, in mathcomp.boot.prime]
lognSg [prf, in mathcomp.finite_group.fingroup]
lognX [prf, in mathcomp.boot.prime]
lone_subgroup_char [prf, in mathcomp.finite_group.automorphism]
looping_order [prf, in mathcomp.boot.fingraph]
looping_uniq [prf, in mathcomp.boot.path]
loopingP [prf, in mathcomp.boot.path]
lower_semicontinuous_HL_maximal [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
lower_semicontinuous_measurable [prf, in mathcomp.analysis.measurable_realfun]
lower_semicontinuousP [prf, in mathcomp.analysis.normedtype_theory.ereal_normedtype]
lpreim0 [prf, in mathcomp.algebra.vector]
lpreim_cap_limg [prf, in mathcomp.algebra.vector]
lpreimK [prf, in mathcomp.algebra.vector]
lpreimS [prf, in mathcomp.algebra.vector]
lray_closed [prf, in mathcomp.analysis.topology_theory.order_topology]
lray_open [prf, in mathcomp.analysis.topology_theory.order_topology]
lreg_lead [prf, in mathcomp.algebra.poly]
lreg_lead0 [prf, in mathcomp.algebra.poly]
lreg_polyZ_eq0 [prf, in mathcomp.algebra.poly]
lreg_size [prf, in mathcomp.algebra.poly]
lshift0 [prf, in mathcomp.boot.nmodule]
lshift_inj [prf, in mathcomp.boot.fintype]
lsubmx_const [prf, in mathcomp.algebra.matrix]
lsubmx_key [prf, in mathcomp.algebra.matrix]
lsubmxEsub [prf, in mathcomp.algebra.matrix]
lt0 [prf, in mathcomp.reals.signed]
lt0 [prf, in mathcomp.algebra.interval_inference]
lt0_adde [prf, in mathcomp.reals.constructive_ereal]
lt0_exponential_pdf [prf, in mathcomp.analysis.probability_theory.exponential_distribution]
lt0_fin_numE [prf, in mathcomp.reals.constructive_ereal]
lt0_mset [prf, in mathcomp.analysis.measure_theory.probability_measure]
lt0_muleNy [prf, in mathcomp.reals.constructive_ereal]
lt0_muley [prf, in mathcomp.reals.constructive_ereal]
lt0_mulNye [prf, in mathcomp.reals.constructive_ereal]
lt0_mulye [prf, in mathcomp.reals.constructive_ereal]
lt0_norm_powR [prf, in mathcomp.analysis.exp]
lt0_powR1 [prf, in mathcomp.analysis.exp]
lt0b [prf, in mathcomp.boot.ssrnat]
lt0e [prf, in mathcomp.reals.constructive_ereal]
lt0F [prf, in mathcomp.reals.signed]
lt0F [prf, in mathcomp.algebra.interval_inference]
lt0mx [prf, in mathcomp.algebra.mxalgebra]
lt0n [prf, in mathcomp.boot.ssrnat]
lt0n_neq0 [prf, in mathcomp.boot.ssrnat]
lt0y [prf, in mathcomp.reals.constructive_ereal]
lt1 [prf, in mathcomp.algebra.interval_inference]
lt1mx [prf, in mathcomp.algebra.mxalgebra]
lt_atan [prf, in mathcomp.analysis.trigo]
lt_bound_def [prf, in mathcomp.algebra.interval]
lt_def_ereal [prf, in mathcomp.reals.constructive_ereal]
lt_disjoint [prf, in mathcomp.classical.set_interval]
lt_eqmx [prf, in mathcomp.algebra.mxalgebra]
lt_ereal_bnd [prf, in mathcomp.reals.real_interval]
lt_ereal_nbhs [prf, in mathcomp.reals.constructive_ereal]
lt_factor [prf, in mathcomp.classical.set_interval]
lt_in_itv [prf, in mathcomp.algebra.interval]
lt_inf_imfset [prf, in mathcomp.reals.reals]
lt_irrelevance [prf, in mathcomp.boot.ssrnat]
lt_le_nbhsl [prf, in mathcomp.analysis.topology_theory.num_topology]
lt_le_nbhsr [prf, in mathcomp.analysis.topology_theory.num_topology]
lt_lim [prf, in mathcomp.analysis.sequences]
lt_line_path [prf, in mathcomp.classical.set_interval]
lt_min_lt [prf, in mathcomp.classical.unstable]
lt_nbhsl [prf, in mathcomp.analysis.topology_theory.num_topology]
lt_nbhsl_le [prf, in mathcomp.analysis.topology_theory.num_topology]
lt_nbhsl_lt [prf, in mathcomp.analysis.topology_theory.num_topology]
lt_nbhsr [prf, in mathcomp.analysis.topology_theory.num_topology]
lt_ninfty [prf, in mathcomp.algebra.interval]
lt_rat0 [prf, in mathcomp.algebra.rat]
lt_rat_def [prf, in mathcomp.algebra.rat]
lt_ratE [prf, in mathcomp.algebra.rat]
lt_size_deriv [prf, in mathcomp.algebra.poly]
lt_succ_Rfloor [prf, in mathcomp.reals.reals]
lt_sum_lim_series [prf, in mathcomp.analysis.trigo]
lt_sup_imfset [prf, in mathcomp.reals.reals]
ltBRight_leBLeft [prf, in mathcomp.algebra.interval]
ltBSide [prf, in mathcomp.algebra.interval]
lte0 [prf, in mathcomp.reals.constructive_ereal]
lte01 [prf, in mathcomp.reals.constructive_ereal]
lte0_abs [prf, in mathcomp.reals.constructive_ereal]
lte0n [prf, in mathcomp.reals.constructive_ereal]
lte0N1 [prf, in mathcomp.reals.constructive_ereal]
lte1n [prf, in mathcomp.reals.constructive_ereal]
lte_absl [prf, in mathcomp.reals.constructive_ereal]
lte_add_pinfty [prf, in mathcomp.reals.constructive_ereal]
lte_expeR [prf, in mathcomp.analysis.exp]
lte_fin [prf, in mathcomp.reals.constructive_ereal]
lte_leB [prf, in mathcomp.reals.constructive_ereal]
lte_leD [prf, in mathcomp.reals.constructive_ereal]
lte_lim [prf, in mathcomp.analysis.sequences]
lte_lne [prf, in mathcomp.analysis.exp]
lte_mul_pinfty [prf, in mathcomp.reals.constructive_ereal]
lte_ndivlMl [prf, in mathcomp.reals.constructive_ereal]
lte_ndivlMr [prf, in mathcomp.reals.constructive_ereal]
lte_ndivrMl [prf, in mathcomp.reals.constructive_ereal]
lte_ndivrMr [prf, in mathcomp.reals.constructive_ereal]
lte_nmul2l [prf, in mathcomp.reals.constructive_ereal]
lte_nmul2r [prf, in mathcomp.reals.constructive_ereal]
lte_nmull [prf, in mathcomp.reals.constructive_ereal]
lte_nmulr [prf, in mathcomp.reals.constructive_ereal]
lte_paddl [prf, in mathcomp.reals.constructive_ereal]
lte_paddr [prf, in mathcomp.reals.constructive_ereal]
lte_pdivlMl [prf, in mathcomp.reals.constructive_ereal]
lte_pdivlMr [prf, in mathcomp.reals.constructive_ereal]
lte_pdivrMl [prf, in mathcomp.reals.constructive_ereal]
lte_pdivrMr [prf, in mathcomp.reals.constructive_ereal]
lte_pmul [prf, in mathcomp.reals.constructive_ereal]
lte_pmul2l [prf, in mathcomp.reals.constructive_ereal]
lte_pmul2r [prf, in mathcomp.reals.constructive_ereal]
lte_pmull [prf, in mathcomp.reals.constructive_ereal]
lte_pmulr [prf, in mathcomp.reals.constructive_ereal]
lte_pV2 [prf, in mathcomp.reals.constructive_ereal]
lte_spadder [prf, in mathcomp.reals.constructive_ereal]
lte_spaddre [prf, in mathcomp.reals.constructive_ereal]
lte_sqr [prf, in mathcomp.reals.constructive_ereal]
lte_sqrE [prf, in mathcomp.reals.constructive_ereal]
lte_subel_addl [prf, in mathcomp.reals.constructive_ereal]
lte_subel_addr [prf, in mathcomp.reals.constructive_ereal]
lte_suber_addl [prf, in mathcomp.reals.constructive_ereal]
lte_suber_addr [prf, in mathcomp.reals.constructive_ereal]
lte_sum_pinfty [prf, in mathcomp.reals.constructive_ereal]
lte_tofin [prf, in mathcomp.reals.constructive_ereal]
lteBlDl [prf, in mathcomp.reals.constructive_ereal]
lteBlDr [prf, in mathcomp.reals.constructive_ereal]
lteBrDl [prf, in mathcomp.reals.constructive_ereal]
lteBrDr [prf, in mathcomp.reals.constructive_ereal]
lteD [prf, in mathcomp.reals.constructive_ereal]
lteD2lE [prf, in mathcomp.reals.constructive_ereal]
lteD2rE [prf, in mathcomp.reals.constructive_ereal]
lteDl [prf, in mathcomp.reals.constructive_ereal]
lteDr [prf, in mathcomp.reals.constructive_ereal]
ltEereal [prf, in mathcomp.reals.constructive_ereal]
lteif_in_itv [prf, in mathcomp.algebra.interval]
lteifS [prf, in mathcomp.classical.mathcomp_extra]
lteN10 [prf, in mathcomp.reals.constructive_ereal]
lteN2 [prf, in mathcomp.reals.constructive_ereal]
lteNl [prf, in mathcomp.reals.constructive_ereal]
lteNr [prf, in mathcomp.reals.constructive_ereal]
ltey [prf, in mathcomp.reals.constructive_ereal]
ltey_eq [prf, in mathcomp.reals.constructive_ereal]
ltgte_fin_num [prf, in mathcomp.reals.constructive_ereal]
ltmx0 [prf, in mathcomp.algebra.mxalgebra]
ltmx1 [prf, in mathcomp.algebra.mxalgebra]
ltmx_irrefl [prf, in mathcomp.algebra.mxalgebra]
ltmx_sub_trans [prf, in mathcomp.algebra.mxalgebra]
ltmx_trans [prf, in mathcomp.algebra.mxalgebra]
ltmxE [prf, in mathcomp.algebra.mxalgebra]
ltmxEneq [prf, in mathcomp.algebra.mxalgebra]
ltmxErank [prf, in mathcomp.algebra.mxalgebra]
ltmxW [prf, in mathcomp.algebra.mxalgebra]
ltn0 [prf, in mathcomp.boot.ssrnat]
ltn0Sn [prf, in mathcomp.boot.ssrnat]
ltn_add2l [prf, in mathcomp.boot.ssrnat]
ltn_add2r [prf, in mathcomp.boot.ssrnat]
ltn_addl [prf, in mathcomp.boot.ssrnat]
ltn_addr [prf, in mathcomp.boot.ssrnat]
ltn_ceil [prf, in mathcomp.boot.div]
ltn_divLR [prf, in mathcomp.boot.div]
ltn_divRL [prf, in mathcomp.boot.div]
ltn_double [prf, in mathcomp.boot.ssrnat]
ltn_eqF [prf, in mathcomp.boot.ssrnat]
ltn_exp2l [prf, in mathcomp.boot.ssrnat]
ltn_exp2r [prf, in mathcomp.boot.ssrnat]
ltn_expl [prf, in mathcomp.boot.ssrnat]
ltn_fact [prf, in mathcomp.boot.ssrnat]
ltn_geF [prf, in mathcomp.boot.ssrnat]
ltn_gtP [prf, in mathcomp.boot.ssrnat]
ltn_half_double [prf, in mathcomp.boot.ssrnat]
ltn_ind [prf, in mathcomp.boot.ssrnat]
ltn_leq_trans [prf, in mathcomp.boot.ssrnat]
ltn_leqif [prf, in mathcomp.boot.ssrnat]
ltn_log0 [prf, in mathcomp.boot.prime]
ltn_log_quotient [prf, in mathcomp.solvable.pgroup]
ltn_logl [prf, in mathcomp.boot.prime]
ltn_ltP [prf, in mathcomp.boot.ssrnat]
ltn_min [prf, in mathcomp.boot.ssrnat]
ltn_mod [prf, in mathcomp.boot.div]
ltn_morphim [prf, in mathcomp.finite_group.morphism]
ltn_mul [prf, in mathcomp.boot.ssrnat]
ltn_mul2l [prf, in mathcomp.boot.ssrnat]
ltn_mul2r [prf, in mathcomp.boot.ssrnat]
ltn_mull [prf, in mathcomp.boot.ssrnat]
ltn_mulr [prf, in mathcomp.boot.ssrnat]
ltn_neqAle [prf, in mathcomp.boot.ssrnat]
ltn_odd_Frobenius_ker [prf, in mathcomp.solvable.frobenius]
ltn_ord [prf, in mathcomp.boot.fintype]
ltn_Pdiv [prf, in mathcomp.boot.div]
ltn_pdiv2_prime [prf, in mathcomp.boot.prime]
ltn_pexp2l [prf, in mathcomp.boot.ssrnat]
ltn_pfact [prf, in mathcomp.boot.ssrnat]
ltn_pmod [prf, in mathcomp.boot.div]
ltn_pmul2l [prf, in mathcomp.boot.ssrnat]
ltn_pmul2r [prf, in mathcomp.boot.ssrnat]
ltn_Pmull [prf, in mathcomp.boot.ssrnat]
ltn_Pmulr [prf, in mathcomp.boot.ssrnat]
ltn_predK [prf, in mathcomp.boot.ssrnat]
ltn_predL [prf, in mathcomp.boot.ssrnat]
ltn_predRL [prf, in mathcomp.boot.ssrnat]
ltn_psubCl [prf, in mathcomp.boot.ssrnat]
ltn_psubLR [prf, in mathcomp.boot.ssrnat]
ltn_quotient [prf, in mathcomp.finite_group.quotient]
ltn_Sdouble [prf, in mathcomp.boot.ssrnat]
ltn_size_undup [prf, in mathcomp.boot.seq]
ltn_sorted_uniq_leq [prf, in mathcomp.boot.path]
ltn_sqr [prf, in mathcomp.boot.ssrnat]
ltn_sub2l [prf, in mathcomp.boot.ssrnat]
ltn_sub2lE [prf, in mathcomp.boot.ssrnat]
ltn_sub2r [prf, in mathcomp.boot.ssrnat]
ltn_sub2rE [prf, in mathcomp.boot.ssrnat]
ltn_subCl [prf, in mathcomp.boot.ssrnat]
ltn_subCr [prf, in mathcomp.boot.ssrnat]
ltn_subLR [prf, in mathcomp.boot.ssrnat]
ltn_subRL [prf, in mathcomp.boot.ssrnat]
ltn_subrL [prf, in mathcomp.boot.ssrnat]
ltn_subrR [prf, in mathcomp.boot.ssrnat]
ltn_trans [prf, in mathcomp.boot.ssrnat]
ltn_trivIset [prf, in mathcomp.classical.classical_sets]
ltn_unsplit [prf, in mathcomp.boot.fintype]
ltn_uphalf_double [prf, in mathcomp.boot.ssrnat]
ltngtP [prf, in mathcomp.boot.ssrnat]
ltninfty_adde_def [prf, in mathcomp.reals.constructive_ereal]
ltnn [prf, in mathcomp.boot.ssrnat]
ltnNge [prf, in mathcomp.boot.ssrnat]
ltnNleqif [prf, in mathcomp.boot.ssrnat]
ltnP [prf, in mathcomp.boot.ssrnat]
ltnS [prf, in mathcomp.boot.ssrnat]
ltnSE [prf, in mathcomp.boot.ssrnat]
ltnSn [prf, in mathcomp.boot.ssrnat]
ltnW [prf, in mathcomp.boot.ssrnat]
ltnW_homo [prf, in mathcomp.boot.ssrnat]
ltnW_homo_in [prf, in mathcomp.boot.ssrnat]
ltnW_nhomo [prf, in mathcomp.boot.ssrnat]
ltnW_nhomo_in [prf, in mathcomp.boot.ssrnat]
ltNy0 [prf, in mathcomp.reals.constructive_ereal]
ltNye [prf, in mathcomp.reals.constructive_ereal]
ltNye_eq [prf, in mathcomp.reals.constructive_ereal]
ltNyr [prf, in mathcomp.reals.constructive_ereal]
ltNz_nat [prf, in mathcomp.algebra.ssrint]
ltP [prf, in mathcomp.boot.ssrnat]
ltpinfty_adde_def [prf, in mathcomp.reals.constructive_ereal]
ltr0_cvgV0 [prf, in mathcomp.analysis.normedtype_theory.normed_module]
ltr0_derive1_decr [prf, in mathcomp.analysis.derive]
ltr0_derive1_lt [prf, in mathcomp.analysis.derive]
ltr0_derive1_lt_cc [prf, in mathcomp.analysis.derive]
ltr0_derive1_lt_co [prf, in mathcomp.analysis.derive]
ltr0_derive1_lt_oc [prf, in mathcomp.analysis.derive]
ltr0_derive1_lt_oo [prf, in mathcomp.analysis.derive]
ltr0_sgz [prf, in mathcomp.algebra.ssrint]
ltr0q [prf, in mathcomp.algebra.rat]
ltr0z [prf, in mathcomp.algebra.ssrint]
ltr1z [prf, in mathcomp.algebra.ssrint]
ltr_add_invr [prf, in mathcomp.reals.reals]
ltr_bound [prf, in mathcomp.classical.unstable]
ltr_cos [prf, in mathcomp.analysis.trigo]
ltr_expR [prf, in mathcomp.analysis.exp]
ltr_eXz2l [prf, in mathcomp.algebra.ssrint]
ltr_int [prf, in mathcomp.algebra.ssrint]
ltr_ln [prf, in mathcomp.analysis.exp]
ltr_niXz2l [prf, in mathcomp.algebra.ssrint]
ltr_nMz2l [prf, in mathcomp.algebra.ssrint]
ltr_nMz2r [prf, in mathcomp.algebra.ssrint]
ltr_norm_bound [prf, in mathcomp.classical.unstable]
ltr_nXz2r [prf, in mathcomp.algebra.ssrint]
ltr_piXz2l [prf, in mathcomp.algebra.ssrint]
ltr_pMz2l [prf, in mathcomp.algebra.ssrint]
ltr_pMz2r [prf, in mathcomp.algebra.ssrint]
ltr_pXz2r [prf, in mathcomp.algebra.ssrint]
ltr_rat [prf, in mathcomp.algebra.rat]
ltr_sin [prf, in mathcomp.analysis.trigo]
ltr_sum [prf, in mathcomp.classical.unstable]
ltr_sum_nat [prf, in mathcomp.classical.unstable]
ltr_tan [prf, in mathcomp.analysis.trigo]
ltrNbound [prf, in mathcomp.classical.unstable]
ltrq0 [prf, in mathcomp.algebra.rat]
ltry [prf, in mathcomp.reals.constructive_ereal]
ltrz0 [prf, in mathcomp.algebra.ssrint]
ltrz1 [prf, in mathcomp.algebra.ssrint]
lty_fin_num_fun [prf, in mathcomp.analysis.measure_theory.measure_function]
lty_poweRy [prf, in mathcomp.analysis.exp]
ltz0_abs [prf, in mathcomp.algebra.ssrint]
ltz1D [prf, in mathcomp.algebra.ssrint]
ltz_ceil [prf, in mathcomp.algebra.intdiv]
ltz_divLR [prf, in mathcomp.algebra.intdiv]
ltz_divRL [prf, in mathcomp.algebra.intdiv]
ltz_mod [prf, in mathcomp.algebra.intdiv]
ltz_nat [prf, in mathcomp.algebra.ssrint]
ltz_pmod [prf, in mathcomp.algebra.intdiv]
ltzD1 [prf, in mathcomp.algebra.ssrint]
ltzN_nat [prf, in mathcomp.algebra.ssrint]
LUP_card_GL [prf, in mathcomp.algebra.mxalgebra]