'B' (Lemmas)

Files

Definitions

Lemmas

Abbreviations

Global Index

B (Lemmas)

Baire [prf, in mathcomp.analysis.sequences]
ball0 [prf, in mathcomp.analysis.normedtype]
ball_center [prf, in mathcomp.analysis.topology]
ball_close [prf, in mathcomp.analysis.topology]
ball_ereal_ball_fin_le [prf, in mathcomp.analysis.ereal]
ball_ereal_ball_fin_lt [prf, in mathcomp.analysis.ereal]
ball_gt0 [prf, in mathcomp.analysis.normedtype]
ball_hausdorff [prf, in mathcomp.analysis.topology]
ball_inj [prf, in mathcomp.analysis.normedtype]
ball_itv [prf, in mathcomp.analysis.normedtype]
ball_norm_center [prf, in mathcomp.analysis.topology]
ball_norm_dec [prf, in mathcomp.analysis.normedtype]
ball_norm_le [prf, in mathcomp.analysis.normedtype]
ball_norm_sym [prf, in mathcomp.analysis.normedtype]
ball_norm_symmetric [prf, in mathcomp.analysis.topology]
ball_norm_triangle [prf, in mathcomp.analysis.topology]
ball_normE [prf, in mathcomp.analysis.normedtype]
ball_open [prf, in mathcomp.analysis.normedtype]
ball_open_nbhs [prf, in mathcomp.analysis.normedtype]
ball_prod_normE [prf, in mathcomp.analysis.normedtype]
ball_split [prf, in mathcomp.analysis.topology]
ball_splitl [prf, in mathcomp.analysis.topology]
ball_splitr [prf, in mathcomp.analysis.topology]
ball_subspace_ball [prf, in mathcomp.analysis.topology]
ball_sym [prf, in mathcomp.analysis.topology]
ball_symE [prf, in mathcomp.analysis.topology]
ball_triangle [prf, in mathcomp.analysis.topology]
ballE [prf, in mathcomp.analysis.normedtype]
ballxx [prf, in mathcomp.analysis.topology]
banach_fixed_point [prf, in mathcomp.analysis.sequences]
Banach_Steinhauss [prf, in mathcomp.analysis.sequences]
bernoulli_dirac [prf, in mathcomp.analysis.probability]
bernoulli_pmf1 [prf, in mathcomp.analysis.probability]
bernoulli_pmf_ge0 [prf, in mathcomp.analysis.probability]
bernoulliE [prf, in mathcomp.analysis.probability]
big_nat_mul [prf, in mathcomp.analysis.trigo]
big_trivIset [prf, in mathcomp.analysis.measure]
bigcap0 [prf, in mathcomp.classical.classical_sets]
bigcap2E [prf, in mathcomp.classical.classical_sets]
bigcap2inE [prf, in mathcomp.classical.classical_sets]
bigcap_addn [prf, in mathcomp.classical.classical_sets]
bigcap_bigcup [prf, in mathcomp.classical.functions]
bigcap_const [prf, in mathcomp.classical.classical_sets]
bigcap_fset [prf, in mathcomp.classical.classical_sets]
bigcap_fsetD1 [prf, in mathcomp.classical.classical_sets]
bigcap_fsetU1 [prf, in mathcomp.classical.classical_sets]
bigcap_image [prf, in mathcomp.classical.classical_sets]
bigcap_inf [prf, in mathcomp.classical.classical_sets]
bigcap_measurable [prf, in mathcomp.analysis.measure]
bigcap_measurableType [prf, in mathcomp.analysis.measure]
bigcap_mkcond [prf, in mathcomp.classical.classical_sets]
bigcap_mkcondl [prf, in mathcomp.classical.classical_sets]
bigcap_mkcondr [prf, in mathcomp.classical.classical_sets]
bigcap_mkord [prf, in mathcomp.classical.classical_sets]
bigcap_seq [prf, in mathcomp.classical.classical_sets]
bigcap_seq_cond [prf, in mathcomp.classical.classical_sets]
bigcap_set0 [prf, in mathcomp.classical.classical_sets]
bigcap_set1 [prf, in mathcomp.classical.classical_sets]
bigcap_set_type [prf, in mathcomp.classical.classical_sets]
bigcap_setD1 [prf, in mathcomp.classical.classical_sets]
bigcap_setU [prf, in mathcomp.classical.classical_sets]
bigcap_setU1 [prf, in mathcomp.classical.classical_sets]
bigcap_splitn [prf, in mathcomp.classical.classical_sets]
bigcapI [prf, in mathcomp.classical.classical_sets]
bigcapID [prf, in mathcomp.classical.classical_sets]
bigcapIl [prf, in mathcomp.classical.classical_sets]
bigcapIr [prf, in mathcomp.classical.classical_sets]
bigcapT [prf, in mathcomp.classical.classical_sets]
bigcapT_measurable [prf, in mathcomp.analysis.measure]
bigcapTP [prf, in mathcomp.classical.classical_sets]
bigcup0 [prf, in mathcomp.classical.classical_sets]
bigcup0P [prf, in mathcomp.classical.classical_sets]
bigcup2E [prf, in mathcomp.classical.classical_sets]
bigcup2inE [prf, in mathcomp.classical.classical_sets]
bigcup_addn [prf, in mathcomp.classical.classical_sets]
bigcup_ballT [prf, in mathcomp.analysis.normedtype]
bigcup_bigcup [prf, in mathcomp.classical.classical_sets]
bigcup_bigsetU_bigcup [prf, in mathcomp.analysis.sequences]
bigcup_connected [prf, in mathcomp.analysis.topology]
bigcup_const [prf, in mathcomp.classical.classical_sets]
bigcup_countable [prf, in mathcomp.classical.cardinality]
bigcup_finite [prf, in mathcomp.classical.cardinality]
bigcup_fset [prf, in mathcomp.classical.classical_sets]
bigcup_fsetD1 [prf, in mathcomp.classical.classical_sets]
bigcup_fsetU1 [prf, in mathcomp.classical.classical_sets]
bigcup_image [prf, in mathcomp.classical.classical_sets]
bigcup_imset1 [prf, in mathcomp.classical.classical_sets]
bigcup_itvT [prf, in mathcomp.analysis.real_interval]
bigcup_measurable [prf, in mathcomp.analysis.measure]
bigcup_mkcond [prf, in mathcomp.classical.classical_sets]
bigcup_mkcondl [prf, in mathcomp.classical.classical_sets]
bigcup_mkcondr [prf, in mathcomp.classical.classical_sets]
bigcup_mkord [prf, in mathcomp.classical.classical_sets]
bigcup_negative_set [prf, in mathcomp.analysis.charge]
bigcup_nonempty [prf, in mathcomp.classical.classical_sets]
bigcup_ointsub0 [prf, in mathcomp.analysis.normedtype]
bigcup_ointsub_sub [prf, in mathcomp.analysis.normedtype]
bigcup_open [prf, in mathcomp.analysis.topology]
bigcup_pred [prf, in mathcomp.classical.classical_sets]
bigcup_recl [prf, in mathcomp.classical.classical_sets]
bigcup_seq [prf, in mathcomp.classical.classical_sets]
bigcup_seq_cond [prf, in mathcomp.classical.classical_sets]
bigcup_set0 [prf, in mathcomp.classical.classical_sets]
bigcup_set1 [prf, in mathcomp.classical.classical_sets]
bigcup_set_type [prf, in mathcomp.classical.classical_sets]
bigcup_setD1 [prf, in mathcomp.classical.classical_sets]
bigcup_setU [prf, in mathcomp.classical.classical_sets]
bigcup_setU1 [prf, in mathcomp.classical.classical_sets]
bigcup_setX [prf, in mathcomp.classical.classical_sets]
bigcup_setX_dep [prf, in mathcomp.classical.classical_sets]
bigcup_splitn [prf, in mathcomp.classical.classical_sets]
bigcup_sub [prf, in mathcomp.classical.classical_sets]
bigcup_subset [prf, in mathcomp.classical.classical_sets]
bigcup_sup [prf, in mathcomp.classical.classical_sets]
bigcupDr [prf, in mathcomp.classical.classical_sets]
bigcupID [prf, in mathcomp.classical.classical_sets]
bigcupT [prf, in mathcomp.classical.classical_sets]
bigcupT_emeasurable [prf, in mathcomp.analysis.lebesgue_measure]
bigcupT_measurable_rat [prf, in mathcomp.analysis.measure]
bigcupU [prf, in mathcomp.classical.classical_sets]
bigcupUl [prf, in mathcomp.classical.classical_sets]
bigcupUr [prf, in mathcomp.classical.classical_sets]
bigcupX1l [prf, in mathcomp.classical.classical_sets]
bigcupX1r [prf, in mathcomp.classical.classical_sets]
bigfs [prf, in mathcomp.classical.fsbigop]
bigmax_geP [prf, in mathcomp.analysis.topology]
bigmax_gtP [prf, in mathcomp.analysis.topology]
bigmax_nnsfunE [prf, in mathcomp.analysis.lebesgue_integral]
bigmax_sup_seq [prf, in mathcomp.classical.mathcomp_extra]
bigmaxe_fin_num [prf, in mathcomp.analysis.constructive_ereal]
bigmaxr_addr [prf, in mathcomp.analysis.Rstruct]
bigmaxr_cons [prf, in mathcomp.analysis.Rstruct]
bigmaxr_index [prf, in mathcomp.analysis.Rstruct]
bigmaxr_ler [prf, in mathcomp.analysis.Rstruct]
bigmaxr_lerif [prf, in mathcomp.analysis.Rstruct]
bigmaxr_lerP [prf, in mathcomp.analysis.Rstruct]
bigmaxr_ltrP [prf, in mathcomp.analysis.Rstruct]
bigmaxr_mem [prf, in mathcomp.analysis.Rstruct]
bigmaxr_mulr [prf, in mathcomp.analysis.Rstruct]
bigmaxr_nil [prf, in mathcomp.analysis.Rstruct]
bigmaxr_un [prf, in mathcomp.analysis.Rstruct]
bigmaxrE [prf, in mathcomp.analysis.Rstruct]
bigmaxrP [prf, in mathcomp.analysis.Rstruct]
bigmin_leP [prf, in mathcomp.analysis.topology]
bigmin_ltP [prf, in mathcomp.analysis.topology]
bigO [prf, in mathcomp.analysis.landau]
bigO0_subproof [prf, in mathcomp.analysis.landau]
bigO_bigO_eqO [prf, in mathcomp.analysis.landau]
bigO_class [prf, in mathcomp.analysis.landau]
bigO_eqO [prf, in mathcomp.analysis.landau]
bigO_exP [prf, in mathcomp.analysis.landau]
bigO_littleo_eqo [prf, in mathcomp.analysis.landau]
bigOE [prf, in mathcomp.analysis.landau]
bigOmega [prf, in mathcomp.analysis.landau]
bigOmega_class [prf, in mathcomp.analysis.landau]
bigOmega_refl_subproof [prf, in mathcomp.analysis.landau]
bigOmegaP [prf, in mathcomp.analysis.landau]
bigOP [prf, in mathcomp.analysis.landau]
bigrmax_dflt [prf, in mathcomp.analysis.Rstruct]
bigsetI_bigcap2 [prf, in mathcomp.classical.classical_sets]
bigsetI_fset_set [prf, in mathcomp.classical.cardinality]
bigsetI_fset_set_cond [prf, in mathcomp.classical.cardinality]
bigsetI_measurable [prf, in mathcomp.analysis.measure]
bigsetU_bigcup [prf, in mathcomp.classical.classical_sets]
bigsetU_bigcup2 [prf, in mathcomp.classical.classical_sets]
bigsetU_compact [prf, in mathcomp.analysis.topology]
bigsetU_dyadic_itv [prf, in mathcomp.analysis.lebesgue_integral]
bigsetU_fset_set [prf, in mathcomp.classical.cardinality]
bigsetU_fset_set_cond [prf, in mathcomp.classical.cardinality]
bigsetU_measurable [prf, in mathcomp.analysis.measure]
bigsetU_seqD [prf, in mathcomp.analysis.sequences]
bigsetU_seqDU [prf, in mathcomp.analysis.sequences]
bigsetU_sup [prf, in mathcomp.classical.classical_sets]
bigTheta [prf, in mathcomp.analysis.landau]
bigTheta_class [prf, in mathcomp.analysis.landau]
bigTheta_refl_subproof [prf, in mathcomp.analysis.landau]
bigThetaE [prf, in mathcomp.analysis.landau]
bigThetaP [prf, in mathcomp.analysis.landau]
bij [prf, in mathcomp.classical.functions]
bij_II_D1 [prf, in mathcomp.classical.functions]
bij_olift [prf, in mathcomp.classical.functions]
bij_omap [prf, in mathcomp.classical.functions]
bij_sub [prf, in mathcomp.classical.functions]
bij_sub_setUll [prf, in mathcomp.classical.functions]
bij_sub_setUlr [prf, in mathcomp.classical.functions]
bij_sub_setUrl [prf, in mathcomp.classical.functions]
bij_sub_setUrr [prf, in mathcomp.classical.functions]
bij_sub_sym [prf, in mathcomp.classical.functions]
bij_subl [prf, in mathcomp.classical.functions]
bij_subr [prf, in mathcomp.classical.functions]
bijective_contract [prf, in mathcomp.analysis.ereal]
bijPex [prf, in mathcomp.classical.cardinality]
bijpinv_bij [prf, in mathcomp.classical.functions]
bijTT [prf, in mathcomp.classical.functions]
bilinear_eqo [prf, in mathcomp.analysis.derive]
bilinear_schwarz [prf, in mathcomp.analysis.derive]
bin_prob0 [prf, in mathcomp.analysis.probability]
bin_prob1 [prf, in mathcomp.analysis.probability]
binomial_msum [prf, in mathcomp.analysis.probability]
binomial_pmf_ge0 [prf, in mathcomp.analysis.probability]
binomial_probE [prf, in mathcomp.analysis.probability]
bmaxrf_index [prf, in mathcomp.analysis.Rstruct]
bmaxrf_ler [prf, in mathcomp.analysis.Rstruct]
bmaxrf_lerif [prf, in mathcomp.analysis.Rstruct]
bool_compact [prf, in mathcomp.analysis.topology]
bool_nbhs_itv [prf, in mathcomp.analysis.topology]
Boole_inequality [prf, in mathcomp.analysis.measure]
bottom [prf, in mathcomp.analysis.signed]
bound_itvE [prf, in mathcomp.analysis.normedtype]
boundE [prf, in mathcomp.analysis.Rstruct]
bounded_closed_compact [prf, in mathcomp.analysis.normedtype]
bounded_fun_has_lbound [prf, in mathcomp.analysis.normedtype]
bounded_fun_has_lbound_sups [prf, in mathcomp.analysis.sequences]
bounded_fun_has_ubound [prf, in mathcomp.analysis.normedtype]
bounded_fun_has_ubound_infs [prf, in mathcomp.analysis.sequences]
bounded_funD [prf, in mathcomp.analysis.normedtype]
bounded_funN [prf, in mathcomp.analysis.normedtype]
bounded_funP [prf, in mathcomp.analysis.normedtype]
bounded_landau [prf, in mathcomp.analysis.sequences]
bounded_linear_continuous [prf, in mathcomp.analysis.normedtype]
bounded_locally [prf, in mathcomp.analysis.normedtype]
bounded_variation_pos_neg_tvE [prf, in mathcomp.analysis.realfun]
bounded_variationD [prf, in mathcomp.analysis.realfun]
bounded_variationl [prf, in mathcomp.analysis.realfun]
bounded_variationN [prf, in mathcomp.analysis.realfun]
bounded_variationP [prf, in mathcomp.analysis.realfun]
bounded_variationr [prf, in mathcomp.analysis.realfun]
bounded_variationxx [prf, in mathcomp.analysis.realfun]
boundedE [prf, in mathcomp.analysis.normedtype]
Builders_14.mD [prf, in mathcomp.analysis.measure]
Builders_14.mI [prf, in mathcomp.analysis.measure]
Builders_15.funoK [prf, in mathcomp.classical.functions]
Builders_188.sfinite [prf, in mathcomp.analysis.measure]
Builders_20.oinvK [prf, in mathcomp.classical.functions]
Builders_20.oinvS [prf, in mathcomp.classical.functions]
Builders_27.mD [prf, in mathcomp.analysis.measure]
Builders_27.measurableT [prf, in mathcomp.analysis.measure]
Builders_28.finite_subproof [prf, in mathcomp.analysis.numfun]
Builders_29.sfinite_subdef [prf, in mathcomp.analysis.kernel]
Builders_312.le_outer_measure [prf, in mathcomp.analysis.measure]
Builders_312.outer_measure_sigma_subadditive [prf, in mathcomp.analysis.measure]
Builders_389.invK [prf, in mathcomp.classical.functions]
Builders_394.exg [prf, in mathcomp.classical.functions]
Builders_42.mC [prf, in mathcomp.analysis.measure]
Builders_42.mU [prf, in mathcomp.analysis.measure]
Builders_461.funoK [prf, in mathcomp.classical.functions]
Builders_478.funK [prf, in mathcomp.classical.functions]
Builders_61.fin_axiom [prf, in mathcomp.classical.classical_sets]
Builders_61.pickleK [prf, in mathcomp.classical.classical_sets]
Builders_70.eq_find [prf, in mathcomp.classical.classical_sets]
Builders_70.eq_opP [prf, in mathcomp.classical.classical_sets]
Builders_70.ex_find [prf, in mathcomp.classical.classical_sets]
Builders_70.findP [prf, in mathcomp.classical.classical_sets]