'L' (Definitions)

Files

G

J

V

Y

Z

_

*

Definitions

_

*

Lemmas

*

Abbreviations

J

K

Y

Z

_

*

Global Index

L (Definitions)

lambda_system [def, in mathcomp.analysis.measure]
landau_bigO_type__canonical__eqtype_SubType [def, in mathcomp.analysis.landau]
landau_bigOmega_type__canonical__eqtype_SubType [def, in mathcomp.analysis.landau]
landau_bigTheta_type__canonical__eqtype_SubType [def, in mathcomp.analysis.landau]
landau_littleo_type__canonical__eqtype_SubType [def, in mathcomp.analysis.landau]
lbound [def, in mathcomp.classical.classical_sets]
le_ereal [def, in mathcomp.reals.constructive_ereal]
le_expandLR [def, in mathcomp.analysis.ereal]
le_expandRL [def, in mathcomp.analysis.ereal]
le_outer_measure [def, in mathcomp.analysis.measure]
lebesgue_integral_f__canonical__cardinality_FImFun [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_f__canonical__HBSimple_SimpleFun [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_f__canonical__lebesgue_integral_MeasurableFun [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_f__canonical__lebesgue_integral_MeasurableFun__76 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_isMeasurableFun__to__lebesgue_integral_isMeasurableFun [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_m1D__canonical__measure_Content [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_m1D__canonical__measure_Measure [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_m2D__canonical__measure_Content [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_m2D__canonical__measure_Measure [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_MeasurableFun__to__lebesgue_integral_isMeasurableFun [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_MeasurableFun__to__lebesgue_integral_isMeasurableFun__129 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_MeasurableFun__to__lebesgue_integral_isMeasurableFun__133 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_MeasurableFun__to__lebesgue_integral_isMeasurableFun__137 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_MeasurableFun__to__lebesgue_integral_isMeasurableFun__141 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_MeasurableFun__to__lebesgue_integral_isMeasurableFun__150 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_MeasurableFun__to__lebesgue_integral_isMeasurableFun__176 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_MeasurableFun__to__lebesgue_integral_isMeasurableFun__179 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_MeasurableFun__to__lebesgue_integral_isMeasurableFun__182 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_MeasurableFun__to__lebesgue_integral_isMeasurableFun__51 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_MeasurableFun__to__lebesgue_integral_isMeasurableFun__56 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_MeasurableFun__to__lebesgue_integral_isMeasurableFun__61 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_MeasurableFun__to__lebesgue_integral_isMeasurableFun__69 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mfun__canonical__GRing_AddClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mfun__canonical__GRing_Mul2Closed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mfun__canonical__GRing_MulClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mfun__canonical__GRing_OppClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mfun__canonical__GRing_Semiring2Closed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mfun__canonical__GRing_SemiringClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mfun__canonical__GRing_SmulClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mfun__canonical__GRing_SubringClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mfun__canonical__GRing_ZmodClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mindic__canonical__cardinality_FImFun [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mindic__canonical__HBNNSimple_NonNegSimpleFun [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mindic__canonical__HBSimple_SimpleFun [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mindic__canonical__lebesgue_integral_MeasurableFun [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_mindic__canonical__lebesgue_integral_NonNegFun [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_NonNegFun__to__lebesgue_integral_isNonNegFun [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_NonNegFun__to__lebesgue_integral_isNonNegFun__192 [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_product_measure1__canonical__measure_Content [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_product_measure1__canonical__measure_Measure [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_product_measure1__canonical__measure_SFiniteMeasure [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_product_measure1__canonical__measure_SigmaFiniteContent [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_product_measure1__canonical__measure_SigmaFiniteMeasure [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_product_measure2__canonical__measure_Content [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_product_measure2__canonical__measure_Measure [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_sfun__canonical__GRing_AddClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_sfun__canonical__GRing_Mul2Closed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_sfun__canonical__GRing_MulClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_sfun__canonical__GRing_OppClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_sfun__canonical__GRing_Semiring2Closed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_sfun__canonical__GRing_SemiringClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_sfun__canonical__GRing_SmulClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_sfun__canonical__GRing_SubringClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_integral_sfun__canonical__GRing_ZmodClosed [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_measure [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_completed_lebesgue_measure__canonical__measure_Content [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_completed_lebesgue_measure__canonical__measure_Measure [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_completed_lebesgue_measure__canonical__measure_SFiniteMeasure [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_completed_lebesgue_measure__canonical__measure_SigmaFiniteContent [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_completed_lebesgue_measure__canonical__measure_SigmaFiniteMeasure [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_elebesgue_measure__canonical__measure_Content [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_elebesgue_measure__canonical__measure_Measure [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_lebesgue_measure__canonical__measure_Content [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_lebesgue_measure__canonical__measure_Measure [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_lebesgue_measure__canonical__measure_SFiniteMeasure [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_lebesgue_measure__canonical__measure_SigmaFiniteContent [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_measure_lebesgue_measure__canonical__measure_SigmaFiniteMeasure [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_pt [def, in mathcomp.analysis.lebesgue_integral]
lebesgue_stieltjes_measure [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_completed_lebesgue_stieltjes_measure__canonical__measure_Content [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_completed_lebesgue_stieltjes_measure__canonical__measure_Measure [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_completed_lebesgue_stieltjes_measure__canonical__measure_SFiniteMeasure [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_completed_lebesgue_stieltjes_measure__canonical__measure_SigmaFiniteContent [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_completed_lebesgue_stieltjes_measure__canonical__measure_SigmaFiniteMeasure [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_lebesgue_stieltjes_measure__canonical__measure_Content [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_lebesgue_stieltjes_measure__canonical__measure_Measure [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_lebesgue_stieltjes_measure__canonical__measure_SFiniteMeasure [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_lebesgue_stieltjes_measure__canonical__measure_SigmaFiniteContent [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_lebesgue_stieltjes_measure__canonical__measure_SigmaFiniteMeasure [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_ocitv_type__canonical__choice_Choice [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_ocitv_type__canonical__classical_sets_Pointed [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_ocitv_type__canonical__eqtype_Equality [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_ocitv_type__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_wlength__canonical__measure_Content [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
lebesgue_stieltjes_measure_wlength__canonical__measure_Measure [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
LebesgueMeasure.HB_unnamed_factory_28 [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.HB_unnamed_factory_30 [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.HB_unnamed_factory_33 [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.HB_unnamed_factory_38 [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.HB_unnamed_mixin_32 [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.HB_unnamed_mixin_36 [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.HB_unnamed_mixin_37 [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.hlength [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.lebesgue_measure [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.LebesgueMeasure_hlength__canonical__measure_Content [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.LebesgueMeasure_hlength__canonical__measure_Measure [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.LebesgueMeasure_lebesgue_measure__canonical__measure_Content [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.LebesgueMeasure_lebesgue_measure__canonical__measure_Measure [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.LebesgueMeasure_lebesgue_measure__canonical__measure_SigmaFiniteContent [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.measure_Content_SigmaSubAdditive_isMeasure__to__measure_Content_isMeasure [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.measure_Measure__to__measure_Content_isMeasure [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.measure_Measure__to__measure_isContent [def, in mathcomp.analysis.lebesgue_measure]
lim [def, in mathcomp.classical.filter]
lim_in [def, in mathcomp.classical.filter]
lim_max_approxRN_seq.charge_isCharge__to__charge_isAdditiveCharge [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.charge_isCharge__to__charge_isSemiSigmaAdditive [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.charge_isCharge__to__measure_isFinite [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.epsRN [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.fRN [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.HB_unnamed_factory_151 [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.HB_unnamed_mixin_155 [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.HB_unnamed_mixin_156 [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.HB_unnamed_mixin_157 [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.lim_max_approxRN_seq_sigmaRN__canonical__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.lim_max_approxRN_seq_sigmaRN__canonical__charge_Charge [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.lim_max_approxRN_seq_sigmaRN__canonical__measure_FinNumFun [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.sigmaRN [def, in mathcomp.analysis.charge]
lim_sup_davg [def, in mathcomp.analysis.lebesgue_integral]
lim_sup_set [def, in mathcomp.analysis.measure]
lime_inf [def, in mathcomp.analysis.realfun]
lime_sup [def, in mathcomp.analysis.realfun]
limf_einf [def, in mathcomp.analysis.normedtype]
limf_esup [def, in mathcomp.analysis.normedtype]
limit_point [def, in mathcomp.analysis.topology_theory.topology_structure]
limn_einf [def, in mathcomp.analysis.sequences]
limn_esup [def, in mathcomp.analysis.sequences]
limn_inf [def, in mathcomp.analysis.sequences]
limn_sup [def, in mathcomp.analysis.sequences]
line_path [def, in mathcomp.classical.set_interval]
Linear_type__canonical__choice_Choice [def, in mathcomp.reals.prodnormedzmodule]
Linear_type__canonical__classical_sets_Pointed [def, in mathcomp.reals.prodnormedzmodule]
Linear_type__canonical__eqtype_Equality [def, in mathcomp.reals.prodnormedzmodule]
linearl_subproof [def, in mathcomp.analysis.forms]
linearr_subproof [def, in mathcomp.analysis.forms]
lipschitz_on [def, in mathcomp.analysis.normedtype]
littleo0 [def, in mathcomp.analysis.landau]
littleo_clone [def, in mathcomp.analysis.landau]
littleo_is_bigO [def, in mathcomp.analysis.landau]
ln [def, in mathcomp.analysis.exp]
Lnorm.body [def, in mathcomp.analysis.hoelder]
Lnorm.unlock [def, in mathcomp.analysis.hoelder]
Lnorm_unlock_subterm [def, in mathcomp.analysis.hoelder]
locally_compact [def, in mathcomp.analysis.topology_theory.compact]
locally_convex [def, in mathcomp.analysis.tvs]
locally_integrable [def, in mathcomp.analysis.lebesgue_integral]
locally_of [def, in mathcomp.analysis.topology_theory.topology_structure]
locked_acos [def, in mathcomp.analysis.trigo]
locked_asin [def, in mathcomp.analysis.trigo]
locked_atan [def, in mathcomp.analysis.trigo]
locked_cos [def, in mathcomp.analysis.trigo]
locked_Lnorm [def, in mathcomp.analysis.hoelder]
locked_sin [def, in mathcomp.analysis.trigo]
Logic_False__canonical__choice_Choice [def, in mathcomp.classical.classical_sets]
Logic_False__canonical__choice_Countable [def, in mathcomp.classical.classical_sets]
Logic_False__canonical__classical_sets_Empty [def, in mathcomp.classical.classical_sets]
Logic_False__canonical__eqtype_Equality [def, in mathcomp.classical.classical_sets]
Logic_False__canonical__fintype_Finite [def, in mathcomp.classical.classical_sets]
lower_bound [def, in mathcomp.classical.wochoice]
lower_semicontinuous [def, in mathcomp.analysis.normedtype]
lt_contract [def, in mathcomp.reals.constructive_ereal]
lt_ereal [def, in mathcomp.reals.constructive_ereal]
lt_expand [def, in mathcomp.reals.constructive_ereal]
lt_expandLR [def, in mathcomp.analysis.ereal]
lt_expandRL [def, in mathcomp.analysis.ereal]
lteey [def, in mathcomp.reals.constructive_ereal]
lteNye [def, in mathcomp.reals.constructive_ereal]