B (Definitions)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Notations |
B (Definitions)
ball [def, in mathcomp.analysis.topology_theory.pseudometric_structure]ball_ [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
ballEmdist [def, in mathcomp.analysis.topology_theory.metric_structure]
baseAspace [def, in mathcomp.field.fieldext]
baseField_scale [def, in mathcomp.field.fieldext]
baseFieldType [def, in mathcomp.field.fieldext]
BaseGroup.pack_ [def, in mathcomp.boot.monoid]
BaseGroup.phant_clone [def, in mathcomp.boot.monoid]
BaseGroup.phant_on_ [def, in mathcomp.boot.monoid]
BaseUMagma.pack_ [def, in mathcomp.boot.monoid]
BaseUMagma.phant_clone [def, in mathcomp.boot.monoid]
BaseUMagma.phant_on_ [def, in mathcomp.boot.monoid]
BaseUMagma_isUMagma.identity_builder [def, in mathcomp.boot.monoid]
BaseUMagma_isUMagma.phant_axioms [def, in mathcomp.boot.monoid]
BaseUMagma_isUMagma.phant_Build [def, in mathcomp.boot.monoid]
baseVspace [def, in mathcomp.field.fieldext]
basis [def, in mathcomp.analysis.topology_theory.topology_structure]
basis_of [def, in mathcomp.algebra.vector]
behead [def, in mathcomp.boot.seq]
behead_bseq [def, in mathcomp.boot.tuple]
behead_tuple [def, in mathcomp.boot.tuple]
belast [def, in mathcomp.boot.seq]
belast_bseq [def, in mathcomp.boot.tuple]
belast_tuple [def, in mathcomp.boot.tuple]
bernoulli_pmf [def, in mathcomp.analysis.probability_theory.bernoulli_distribution]
bernoulli_prob [def, in mathcomp.analysis.probability_theory.bernoulli_distribution]
beta_fun [def, in mathcomp.analysis.probability_theory.beta_distribution]
beta_pdf [def, in mathcomp.analysis.probability_theory.beta_distribution]
beta_prob [def, in mathcomp.analysis.probability_theory.beta_distribution]
beta_prob_bernoulli_prob [def, in mathcomp.analysis.probability_theory.beta_distribution]
Bezout_rec [def, in mathcomp.boot.div]
bgFunc_id [def, in mathcomp.solvable.gfunctor]
big_lexi_le [def, in mathcomp.classical.classical_orders]
big_lexi_order [def, in mathcomp.classical.classical_orders]
bigcap [def, in mathcomp.classical.classical_sets]
bigcap2 [def, in mathcomp.classical.classical_sets]
bigcap_group [def, in mathcomp.finite_group.fingroup]
bigcup [def, in mathcomp.classical.classical_sets]
bigcup2 [def, in mathcomp.classical.classical_sets]
bigcup_ointsub [def, in mathcomp.analysis.normedtype_theory.num_normedtype]
bigcupT_measurable [def, in mathcomp.analysis.measure_theory.measurable_structure]
BigEnough.big_enough_nat [def, in mathcomp.bigenough.bigenough]
BigEnough.big_rel_leq_class [def, in mathcomp.bigenough.bigenough]
BigEnough.bigger_than_of [def, in mathcomp.bigenough.bigenough]
BigEnough.closed [def, in mathcomp.bigenough.bigenough]
BigEnough.leq_big_internal_of [def, in mathcomp.bigenough.bigenough]
bigmax_nnsfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
bigO0 [def, in mathcomp.analysis.landau]
bigO_clone [def, in mathcomp.analysis.landau]
bigOmega_clone [def, in mathcomp.analysis.landau]
bigOmega_refl [def, in mathcomp.analysis.landau]
bigop.body [def, in mathcomp.boot.bigop]
bigop.unlock [def, in mathcomp.boot.bigop]
bigop_unlock [def, in mathcomp.boot.bigop]
bigop_unlock_subterm [def, in mathcomp.boot.bigop]
bigTheta_clone [def, in mathcomp.analysis.landau]
bigTheta_refl [def, in mathcomp.analysis.landau]
Bij.Exports.join_functions_Bij_between_functions_Inject_and_functions_Surject [def, in mathcomp.classical.functions]
Bij.Exports.join_functions_Bij_between_functions_Inject_and_functions_SurjFun [def, in mathcomp.classical.functions]
Bij.Exports.join_functions_Bij_between_functions_InjFun_and_functions_Surject [def, in mathcomp.classical.functions]
Bij.Exports.join_functions_Bij_between_functions_InjFun_and_functions_SurjFun [def, in mathcomp.classical.functions]
Bij.pack_ [def, in mathcomp.classical.functions]
Bij.phant_clone [def, in mathcomp.classical.functions]
Bij.phant_on_ [def, in mathcomp.classical.functions]
bij_of_set_bijection [def, in mathcomp.classical.functions]
bijection_of_bijective [def, in mathcomp.classical.functions]
BijTT.phant_axioms [def, in mathcomp.classical.functions]
BijTT.phant_Build [def, in mathcomp.classical.functions]
Bilinear.pack_ [def, in mathcomp.algebra.sesquilinear]
Bilinear.phant_clone [def, in mathcomp.algebra.sesquilinear]
Bilinear.phant_on_ [def, in mathcomp.algebra.sesquilinear]
bilinear_for [def, in mathcomp.algebra.sesquilinear]
bilinear_isBilinear.phant_axioms [def, in mathcomp.algebra.sesquilinear]
bilinear_isBilinear.phant_Build [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.map_at_both [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.map_at_left [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.map_at_right [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.map_class [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.unify_map_at_both [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.unify_map_at_left [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.unify_map_at_right [def, in mathcomp.algebra.sesquilinear]
BilinearExports.Bilinear.wrap [def, in mathcomp.algebra.sesquilinear]
bin_of_nat [def, in mathcomp.boot.ssrnat]
bin_prob [def, in mathcomp.analysis.probability_theory.binomial_distribution]
binary_addv_expr [def, in mathcomp.algebra.vector]
binary_mxsum_expr [def, in mathcomp.algebra.mxalgebra]
binomial [def, in mathcomp.boot.binomial]
binomial_pmf [def, in mathcomp.analysis.probability_theory.binomial_distribution]
binomial_prob [def, in mathcomp.analysis.probability_theory.binomial_distribution]
BiPointed.pack_ [def, in mathcomp.classical.classical_sets]
BiPointed.phant_clone [def, in mathcomp.classical.classical_sets]
BiPointed.phant_on_ [def, in mathcomp.classical.classical_sets]
BiPointedTopological.Exports.join_topology_structure_BiPointedTopological_between_classical_sets_BiPointed_and_filter_Filtered [def, in mathcomp.analysis.topology_theory.topology_structure]
BiPointedTopological.Exports.join_topology_structure_BiPointedTopological_between_classical_sets_BiPointed_and_filter_Nbhs [def, in mathcomp.analysis.topology_theory.topology_structure]
BiPointedTopological.Exports.join_topology_structure_BiPointedTopological_between_classical_sets_BiPointed_and_topology_structure_Topological [def, in mathcomp.analysis.topology_theory.topology_structure]
BiPointedTopological.pack_ [def, in mathcomp.analysis.topology_theory.topology_structure]
BiPointedTopological.phant_clone [def, in mathcomp.analysis.topology_theory.topology_structure]
BiPointedTopological.phant_on_ [def, in mathcomp.analysis.topology_theory.topology_structure]
bitseq [def, in mathcomp.boot.seq]
bitseq_predType [def, in mathcomp.boot.seq]
block_mx [def, in mathcomp.algebra.matrix]
block_mxAx [def, in mathcomp.algebra.matrix]
bnd_simp [def, in mathcomp.algebra.interval]
bound_in_itv [def, in mathcomp.algebra.interval]
bound_join [def, in mathcomp.algebra.interval]
bound_meet [def, in mathcomp.algebra.interval]
bound_side [def, in mathcomp.classical.unstable]
bounded_fun_norm [def, in mathcomp.analysis.sequences]
bounded_near [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
bounded_variation [def, in mathcomp.analysis.numfun]
bpwedge_shared_pt [def, in mathcomp.analysis.homotopy_theory.wedge_sigT]
branch_apx [def, in mathcomp.analysis.cantor]
bseq [def, in mathcomp.boot.tuple]
bseq_hasChoice [def, in mathcomp.boot.tuple]
bseq_hasDecEq [def, in mathcomp.boot.tuple]
bseq_isCountable [def, in mathcomp.boot.tuple]
bseq_of_tuple [def, in mathcomp.boot.tuple]
bseq_predType [def, in mathcomp.boot.tuple]
bseq_tagged_tuple [def, in mathcomp.boot.tuple]
Build_ProperFilter_ex [def, in mathcomp.classical.filter]
Builders_1.i [def, in mathcomp.field.algC]
Builders_1.le [def, in mathcomp.field.algC]
Builders_1.lt [def, in mathcomp.field.algC]
Builders_1.norm [def, in mathcomp.field.algC]
Builders_1.open_of_nbhs [def, in mathcomp.analysis.topology_theory.topology_structure]
Builders_1.sqrt [def, in mathcomp.field.algC]
Builders_1.v2r [def, in mathcomp.algebra.vector]
Builders_14.open_from [def, in mathcomp.analysis.topology_theory.topology_structure]
Builders_26.sub_enum [def, in mathcomp.boot.fintype]
Builders_26.SubFinMixin [def, in mathcomp.boot.fintype]
Builders_27.T_isRingOfSets [def, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_29.entourage [def, in mathcomp.analysis.normedtype_theory.tvs]
Builders_64.pickle [def, in mathcomp.classical.classical_sets]
Builders_64.unpickle [def, in mathcomp.classical.classical_sets]
Builders_73.eq_op [def, in mathcomp.classical.classical_sets]
Builders_73.find [def, in mathcomp.classical.classical_sets]
bump [def, in mathcomp.boot.fintype]