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]
band [abbrev, in mathcomp.algebra.mxpoly]
BaseFinGroup [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup.arg_sort [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup.clone [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup.copy [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup.on [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup.sort [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup_isGroup [abbrev, in mathcomp.finite_group.fingroup]
BaseFinGroup_isGroup.Build [abbrev, in mathcomp.finite_group.fingroup]
baseFinGroupType [abbrev, in mathcomp.finite_group.fingroup]
BaseGroup [abbrev, in mathcomp.boot.monoid]
BaseGroup.clone [abbrev, in mathcomp.boot.monoid]
BaseGroup.copy [abbrev, in mathcomp.boot.monoid]
BaseGroup.Exports.baseGroupType [abbrev, in mathcomp.boot.monoid]
BaseGroup.on [abbrev, in mathcomp.boot.monoid]
BaseGroup.on_ [abbrev, in mathcomp.boot.monoid]
BaseUMagma [abbrev, in mathcomp.boot.monoid]
BaseUMagma.clone [abbrev, in mathcomp.boot.monoid]
BaseUMagma.copy [abbrev, in mathcomp.boot.monoid]
BaseUMagma.Exports.baseUMagmaType [abbrev, in mathcomp.boot.monoid]
BaseUMagma.on [abbrev, in mathcomp.boot.monoid]
BaseUMagma.on_ [abbrev, in mathcomp.boot.monoid]
BaseUMagma_isUMagma [abbrev, in mathcomp.boot.monoid]
BaseUMagma_isUMagma.axioms [abbrev, in mathcomp.boot.monoid]
BaseUMagma_isUMagma.Build [abbrev, in mathcomp.boot.monoid]
bernoulli [abbrev, in mathcomp.analysis.probability_theory.bernoulli_distribution]
BIG_F [abbrev, in mathcomp.boot.bigop]
big_ord1 [abbrev, in mathcomp.algebra.zmodp]
big_ord1_cond [abbrev, in mathcomp.algebra.zmodp]
BIG_P [abbrev, in mathcomp.boot.bigop]
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]
BigEnough.bigger_than [abbrev, in mathcomp.bigenough.bigenough]
BigEnough.leq_big_internal [abbrev, in mathcomp.bigenough.bigenough]
bigmax_sup_seq [abbrev, in mathcomp.boot.bigop]
bigop [abbrev, in mathcomp.boot.bigop]
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]
Bilinear [abbrev, in mathcomp.algebra.sesquilinear]
Bilinear.clone [abbrev, in mathcomp.algebra.sesquilinear]
Bilinear.copy [abbrev, in mathcomp.algebra.sesquilinear]
Bilinear.Exports.bilinear [abbrev, in mathcomp.algebra.sesquilinear]
Bilinear.on [abbrev, in mathcomp.algebra.sesquilinear]
Bilinear.on_ [abbrev, in mathcomp.algebra.sesquilinear]
bilinear_isBilinear [abbrev, in mathcomp.algebra.sesquilinear]
bilinear_isBilinear.axioms [abbrev, in mathcomp.algebra.sesquilinear]
bilinear_isBilinear.Build [abbrev, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.bilinear [abbrev, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.biscalar [abbrev, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.mapUUV [abbrev, in mathcomp.algebra.sesquilinear]
binomial [abbrev, in mathcomp.analysis.probability_theory.binomial_distribution]
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]
BLeft [abbrev, in mathcomp.algebra.interval]
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]
BRight [abbrev, in mathcomp.algebra.interval]
bsCA [abbrev, in mathcomp.boot.seq]
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.conj [abbrev, in mathcomp.field.algC]
Builders_1.conj_nt [abbrev, in mathcomp.field.algC]
Builders_1.conjK [abbrev, in mathcomp.field.algC]
Builders_1.dim [abbrev, in mathcomp.algebra.vector]
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.finite_group.fingroup]
Builders_1.inv [abbrev, in mathcomp.classical.functions]
Builders_1.mdist [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
Builders_1.mdist_norm [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
Builders_1.mdist_positivity [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
Builders_1.mdist_sym [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
Builders_1.mdist_triangle [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
Builders_1.mdistxx [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
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.mul [abbrev, in mathcomp.finite_group.fingroup]
Builders_1.mul [abbrev, in mathcomp.boot.monoid]
Builders_1.mul1g [abbrev, in mathcomp.finite_group.fingroup]
Builders_1.mulgA [abbrev, in mathcomp.finite_group.fingroup]
Builders_1.mulgA [abbrev, in mathcomp.boot.monoid]
Builders_1.mulVg [abbrev, in mathcomp.finite_group.fingroup]
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.one [abbrev, in mathcomp.finite_group.fingroup]
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.solve_monicpoly [abbrev, in mathcomp.field.closed_field]
Builders_1.sprobability_setT [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
Builders_1.sub_continuous [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
Builders_1.subset_outer_measure_sigma_subadditive [abbrev, in mathcomp.analysis.measure_theory.measure_extension]
Builders_1.vector_subdef [abbrev, in mathcomp.algebra.vector]
Builders_10.mul1g [abbrev, in mathcomp.boot.monoid]
Builders_10.mulg1 [abbrev, in mathcomp.boot.monoid]
Builders_10.one [abbrev, in mathcomp.boot.monoid]
Builders_108.s_finite [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Builders_13.normal_field_splitting_axiom [abbrev, in mathcomp.field.galois]
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.normedtype_theory.tvs]
Builders_17.mul1g [abbrev, in mathcomp.boot.monoid]
Builders_17.mulg1 [abbrev, in mathcomp.boot.monoid]
Builders_17.one [abbrev, in mathcomp.boot.monoid]
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.normedtype_theory.tvs]
Builders_23.mulgA [abbrev, in mathcomp.boot.monoid]
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_28.mul [abbrev, in mathcomp.boot.monoid]
Builders_28.mul1g [abbrev, in mathcomp.boot.monoid]
Builders_28.mulg1 [abbrev, in mathcomp.boot.monoid]
Builders_28.mulgA [abbrev, in mathcomp.boot.monoid]
Builders_28.one [abbrev, in mathcomp.boot.monoid]
Builders_29.add_continuous [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
Builders_29.locally_convex [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
Builders_29.scale_continuous [abbrev, in mathcomp.analysis.normedtype_theory.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_41.inv [abbrev, in mathcomp.boot.monoid]
Builders_41.invgK [abbrev, in mathcomp.boot.monoid]
Builders_41.invgM [abbrev, in mathcomp.boot.monoid]
Builders_41.mul [abbrev, in mathcomp.boot.monoid]
Builders_41.mul1g [abbrev, in mathcomp.boot.monoid]
Builders_41.mulgA [abbrev, in mathcomp.boot.monoid]
Builders_41.one [abbrev, in mathcomp.boot.monoid]
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_53.mulgV [abbrev, in mathcomp.boot.monoid]
Builders_53.mulVg [abbrev, in mathcomp.boot.monoid]
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.inv [abbrev, in mathcomp.boot.monoid]
Builders_60.mul [abbrev, in mathcomp.boot.monoid]
Builders_60.mul1g [abbrev, in mathcomp.boot.monoid]
Builders_60.mulg1 [abbrev, in mathcomp.boot.monoid]
Builders_60.mulgA [abbrev, in mathcomp.boot.monoid]
Builders_60.mulgV [abbrev, in mathcomp.boot.monoid]
Builders_60.mulVg [abbrev, in mathcomp.boot.monoid]
Builders_60.one [abbrev, in mathcomp.boot.monoid]
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_77.pickle [abbrev, in mathcomp.boot.choice]
Builders_77.pickleK [abbrev, in mathcomp.boot.choice]
Builders_77.unpickle [abbrev, in mathcomp.boot.choice]
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.normedtype_theory.tvs]
Builders_82.fin_num_measure [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Builders_82.gmulfF [abbrev, in mathcomp.boot.monoid]
Builders_88.fin_num_measure [abbrev, in mathcomp.analysis.charge]
Builders_972.ler_normD [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
Builders_972.norm [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
Builders_972.normr0_eq0 [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
Builders_972.normrZ [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
BV [abbrev, in mathcomp.analysis.realfun]
BV [abbrev, in mathcomp.analysis.realfun]
BV [abbrev, in mathcomp.analysis.numfun]