B (Abbreviations)

Files

Definitions

Lemmas

Abbreviations

Global Index

B (Abbreviations)

b [abbrev, in mathcomp.classical.functions]
B [abbrev, in mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation]
ball_norm [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
bernoulli [abbrev, in mathcomp.analysis.probability]
bigcap_fset_set [abbrev, in mathcomp.classical.cardinality]
bigcup_fset_set [abbrev, in mathcomp.classical.cardinality]
bigcup_fset_set_cond [abbrev, in mathcomp.classical.cardinality]
bigcup_setM [abbrev, in mathcomp.classical.classical_sets]
bigcup_setM_dep [abbrev, in mathcomp.classical.classical_sets]
bigcupM1l [abbrev, in mathcomp.classical.classical_sets]
bigcupM1r [abbrev, in mathcomp.classical.classical_sets]
Bij [abbrev, in mathcomp.classical.functions]
Bij.clone [abbrev, in mathcomp.classical.functions]
Bij.copy [abbrev, in mathcomp.classical.functions]
Bij.on [abbrev, in mathcomp.classical.functions]
Bij.on_ [abbrev, in mathcomp.classical.functions]
BijTT [abbrev, in mathcomp.classical.functions]
BijTT.axioms [abbrev, in mathcomp.classical.functions]
BijTT.Build [abbrev, in mathcomp.classical.functions]
binomial [abbrev, in mathcomp.analysis.probability]
BiPointed [abbrev, in mathcomp.classical.classical_sets]
BiPointed.clone [abbrev, in mathcomp.classical.classical_sets]
BiPointed.copy [abbrev, in mathcomp.classical.classical_sets]
BiPointed.Exports.biPointedType [abbrev, in mathcomp.classical.classical_sets]
BiPointed.on [abbrev, in mathcomp.classical.classical_sets]
BiPointed.on_ [abbrev, in mathcomp.classical.classical_sets]
BiPointedTopological [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
BiPointedTopological.clone [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
BiPointedTopological.copy [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
BiPointedTopological.Exports.bpTopologicalType [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
BiPointedTopological.on [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
BiPointedTopological.on_ [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
bounded_fun [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
bounded_set [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
bpwedge [abbrev, in mathcomp.analysis.homotopy_theory.wedge_sigT]
bpwedge [abbrev, in mathcomp.analysis.homotopy_theory.wedge_sigT]
bpwedge_lift [abbrev, in mathcomp.analysis.homotopy_theory.wedge_sigT]
bpwedge_lift [abbrev, in mathcomp.analysis.homotopy_theory.wedge_sigT]
Builders_1.ball [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
Builders_1.ball_center [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
Builders_1.ball_sym [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
Builders_1.ball_triangle [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
Builders_1.bigcupT_measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_1.charge0 [abbrev, in mathcomp.analysis.charge]
Builders_1.charge_finite [abbrev, in mathcomp.analysis.charge]
Builders_1.charge_sigma_additive [abbrev, in mathcomp.analysis.charge]
Builders_1.ent [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
Builders_1.entourage [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Builders_1.entourage_diagonal [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Builders_1.entourage_filter [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Builders_1.entourage_inv [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Builders_1.entourage_split_ex [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Builders_1.entourageE [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
Builders_1.inv [abbrev, in mathcomp.classical.functions]
Builders_1.measure0 [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Builders_1.measure_ge0 [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Builders_1.measure_semi_sigma_additive [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Builders_1.nbhs_filter [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_1.nbhs_nbhs [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_1.nbhs_principalE [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
Builders_1.nbhs_singleton [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_1.nbhsE [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Builders_1.nbhsE [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
Builders_1.normrZ [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
Builders_1.outer_measure0 [abbrev, in mathcomp.analysis.measure_theory.measure_extension]
Builders_1.outer_measure_ge0 [abbrev, in mathcomp.analysis.measure_theory.measure_extension]
Builders_1.sprobability_setT [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Builders_1.sub_continuous [abbrev, in mathcomp.analysis.tvs]
Builders_1.subset_outer_measure_sigma_subadditive [abbrev, in mathcomp.analysis.measure_theory.measure_extension]
Builders_1000.ler_normD [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
Builders_1000.norm [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
Builders_1000.normr0_eq0 [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
Builders_1000.normrZ [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
Builders_108.s_finite [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Builders_14.b [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_14.b_cover [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_14.b_join [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_14.D [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_14.I [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_14.measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_14.measurable0 [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_14.measurableD [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_14.measurableU [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_15.funK [abbrev, in mathcomp.classical.functions]
Builders_15.sub_unif_continuous [abbrev, in mathcomp.analysis.tvs]
Builders_19.nbhs [abbrev, in mathcomp.classical.filter]
Builders_20.invK [abbrev, in mathcomp.classical.functions]
Builders_20.invS [abbrev, in mathcomp.classical.functions]
Builders_21.b [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_21.D [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_21.finI_from [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_21.I [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_21.measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_21.measurable_nonempty [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_21.measurable_setI [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_21.measurable_setY [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_22.scale_unif_continuous [abbrev, in mathcomp.analysis.tvs]
Builders_23.probability_setT [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Builders_27.measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_27.measurable0 [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_27.measurableC [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_27.measurableU [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_29.add_continuous [abbrev, in mathcomp.analysis.tvs]
Builders_29.locally_convex [abbrev, in mathcomp.analysis.tvs]
Builders_29.scale_continuous [abbrev, in mathcomp.analysis.tvs]
Builders_30.fimfunE [abbrev, in mathcomp.analysis.numfun]
Builders_336.inv [abbrev, in mathcomp.classical.functions]
Builders_336.invK [abbrev, in mathcomp.classical.functions]
Builders_336.invS [abbrev, in mathcomp.classical.functions]
Builders_34.measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_34.measurableD [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_34.measurableT [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_344.funoK [abbrev, in mathcomp.classical.functions]
Builders_344.funS [abbrev, in mathcomp.classical.functions]
Builders_344.oinvK [abbrev, in mathcomp.classical.functions]
Builders_344.oinvS [abbrev, in mathcomp.classical.functions]
Builders_353.funoK [abbrev, in mathcomp.classical.functions]
Builders_353.funS [abbrev, in mathcomp.classical.functions]
Builders_353.oinv [abbrev, in mathcomp.classical.functions]
Builders_353.oinvK [abbrev, in mathcomp.classical.functions]
Builders_353.oinvS [abbrev, in mathcomp.classical.functions]
Builders_362.funK [abbrev, in mathcomp.classical.functions]
Builders_362.inv [abbrev, in mathcomp.classical.functions]
Builders_370.funK [abbrev, in mathcomp.classical.functions]
Builders_370.funS [abbrev, in mathcomp.classical.functions]
Builders_370.invK [abbrev, in mathcomp.classical.functions]
Builders_370.invS [abbrev, in mathcomp.classical.functions]
Builders_379.funK [abbrev, in mathcomp.classical.functions]
Builders_379.funS [abbrev, in mathcomp.classical.functions]
Builders_379.inv [abbrev, in mathcomp.classical.functions]
Builders_379.invK [abbrev, in mathcomp.classical.functions]
Builders_379.invS [abbrev, in mathcomp.classical.functions]
Builders_389.injV [abbrev, in mathcomp.classical.functions]
Builders_389.invS [abbrev, in mathcomp.classical.functions]
Builders_394.bij [abbrev, in mathcomp.classical.functions]
Builders_42.measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_42.measurable0 [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_42.measurable_bigcup [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_42.measurableC [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_43.sfinite [abbrev, in mathcomp.analysis.kernel]
Builders_461.inj [abbrev, in mathcomp.classical.functions]
Builders_468.inj [abbrev, in mathcomp.classical.functions]
Builders_478.inj [abbrev, in mathcomp.classical.functions]
Builders_5.measure_uub [abbrev, in mathcomp.analysis.kernel]
Builders_50.sprob_kernel [abbrev, in mathcomp.analysis.kernel]
Builders_55.measure_sigma_subadditive [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Builders_6.bigcupT_measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_6.d [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
Builders_6.measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_6.measurable0 [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_6.measurableD [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_6.op [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_6.op_bigU [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_6.opI [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_6.opT [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
Builders_60.prob_kernel [abbrev, in mathcomp.analysis.kernel]
Builders_64.axiom [abbrev, in mathcomp.classical.classical_sets]
Builders_69.sigma_finiteT [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Builders_73.axiom [abbrev, in mathcomp.classical.classical_sets]
Builders_8.entourage [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Builders_8.entourage_diagonal [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Builders_8.entourage_filter [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Builders_8.entourage_inv [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Builders_8.entourage_split_ex [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Builders_8.oinv [abbrev, in mathcomp.classical.functions]
Builders_8.oinvK [abbrev, in mathcomp.classical.functions]
Builders_8.oinvS [abbrev, in mathcomp.classical.functions]
Builders_8.scale_continuous [abbrev, in mathcomp.analysis.tvs]
Builders_82.fin_num_measure [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Builders_88.fin_num_measure [abbrev, in mathcomp.analysis.charge]
BV [abbrev, in mathcomp.analysis.realfun]
BV [abbrev, in mathcomp.analysis.realfun]
BV [abbrev, in mathcomp.analysis.realfun]