'B' (Definitions)

Files

G

J

O

Q

U

V

W

X

Y

Z

_

*

Definitions

_

*

Lemmas

*

Abbreviations

J

K

Y

Z

_

*

Global Index

B (Definitions)

ball [def, in mathcomp.analysis.topology]
ball_ [def, in mathcomp.analysis.topology]
ball_center_subproof [def, in mathcomp.analysis.topology]
ball_sym_subproof [def, in mathcomp.analysis.topology]
ball_triangle_subproof [def, in mathcomp.analysis.topology]
basis [def, in mathcomp.analysis.topology]
bernoulli [def, in mathcomp.analysis.probability]
bernoulli_pmf [def, in mathcomp.analysis.probability]
bigcap [def, in mathcomp.classical.classical_sets]
bigcap2 [def, in mathcomp.classical.classical_sets]
bigcup [def, in mathcomp.classical.classical_sets]
bigcup2 [def, in mathcomp.classical.classical_sets]
bigcup_ointsub [def, in mathcomp.analysis.normedtype]
bigcupT_measurable [def, in mathcomp.analysis.measure]
bigmax_nnsfun [def, in mathcomp.analysis.lebesgue_integral]
bigmaxr [def, in mathcomp.analysis.Rstruct]
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]
bigTheta_clone [def, in mathcomp.analysis.landau]
bigTheta_refl [def, in mathcomp.analysis.landau]
Bij.Exports.functions_Bij__to__functions_Fun [def, in mathcomp.classical.functions]
Bij.Exports.functions_Bij__to__functions_Inject [def, in mathcomp.classical.functions]
Bij.Exports.functions_Bij__to__functions_InjFun [def, in mathcomp.classical.functions]
Bij.Exports.functions_Bij__to__functions_OInversible [def, in mathcomp.classical.functions]
Bij.Exports.functions_Bij__to__functions_OInvFun [def, in mathcomp.classical.functions]
Bij.Exports.functions_Bij__to__functions_Surject [def, in mathcomp.classical.functions]
Bij.Exports.functions_Bij__to__functions_SurjFun [def, in mathcomp.classical.functions]
Bij.Exports.functions_Bij_class__to__functions_Fun_class [def, in mathcomp.classical.functions]
Bij.Exports.functions_Bij_class__to__functions_Inject_class [def, in mathcomp.classical.functions]
Bij.Exports.functions_Bij_class__to__functions_InjFun_class [def, in mathcomp.classical.functions]
Bij.Exports.functions_Bij_class__to__functions_OInversible_class [def, in mathcomp.classical.functions]
Bij.Exports.functions_Bij_class__to__functions_OInvFun_class [def, in mathcomp.classical.functions]
Bij.Exports.functions_Bij_class__to__functions_Surject_class [def, in mathcomp.classical.functions]
Bij.Exports.functions_Bij_class__to__functions_SurjFun_class [def, in mathcomp.classical.functions]
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.analysis.forms]
Bilinear.phant_clone [def, in mathcomp.analysis.forms]
Bilinear.phant_on_ [def, in mathcomp.analysis.forms]
bilinear_for [def, in mathcomp.analysis.forms]
bilinear_isBilinear.phant_axioms [def, in mathcomp.analysis.forms]
bilinear_isBilinear.phant_Build [def, in mathcomp.analysis.forms]
Bilinear_sort__canonical__GRing_Additive [def, in mathcomp.analysis.forms]
Bilinear_sort__canonical__GRing_Linear [def, in mathcomp.analysis.forms]
BilinearExports.Bilinear.map [def, in mathcomp.analysis.forms]
bin_prob [def, in mathcomp.analysis.probability]
binomial_pmf [def, in mathcomp.analysis.probability]
binomial_prob [def, in mathcomp.analysis.probability]
bmaxrf [def, in mathcomp.analysis.Rstruct]
boolp_classicType__canonical__choice_Choice [def, in mathcomp.classical.boolp]
boolp_classicType__canonical__eqtype_Equality [def, in mathcomp.classical.boolp]
boolp_eclassicType__canonical__choice_Choice [def, in mathcomp.classical.boolp]
boolp_eclassicType__canonical__eqtype_Equality [def, in mathcomp.classical.boolp]
bound_side [def, in mathcomp.classical.mathcomp_extra]
bounded_near [def, in mathcomp.analysis.normedtype]
bounded_variation [def, in mathcomp.analysis.realfun]
branch_apx [def, in mathcomp.analysis.cantor]
Build_ProperFilter [def, in mathcomp.analysis.topology]
Builders_1.Builders_1_f__canonical__forms_Bilinear [def, in mathcomp.analysis.forms]
Builders_1.Builders_1_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_1.Builders_1_mu__canonical__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
Builders_1.Builders_1_mu__canonical__charge_Charge [def, in mathcomp.analysis.charge]
Builders_1.Builders_1_mu__canonical__measure_FinNumFun [def, in mathcomp.analysis.charge]
Builders_1.Builders_1_T__canonical__choice_Choice [def, in mathcomp.analysis.measure]
Builders_1.Builders_1_T__canonical__classical_sets_Pointed [def, in mathcomp.analysis.measure]
Builders_1.Builders_1_T__canonical__eqtype_Equality [def, in mathcomp.analysis.measure]
Builders_1.Builders_1_T__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
Builders_1.Builders_1_T__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
Builders_1.HB_unnamed_factory_3 [def, in mathcomp.analysis.forms]
Builders_1.HB_unnamed_factory_3 [def, in mathcomp.analysis.charge]
Builders_1.HB_unnamed_factory_3 [def, in mathcomp.classical.functions]
Builders_1.HB_unnamed_factory_3 [def, in mathcomp.analysis.measure]
Builders_1.HB_unnamed_factory_5 [def, in mathcomp.analysis.charge]
Builders_1.HB_unnamed_factory_5 [def, in mathcomp.classical.functions]
Builders_1.HB_unnamed_factory_7 [def, in mathcomp.analysis.charge]
Builders_100.Builders_100_T__canonical__choice_Choice [def, in mathcomp.analysis.topology]
Builders_100.Builders_100_T__canonical__classical_sets_Pointed [def, in mathcomp.analysis.topology]
Builders_100.Builders_100_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology]
Builders_100.Builders_100_T__canonical__topology_Filtered [def, in mathcomp.analysis.topology]
Builders_100.Builders_100_T__canonical__topology_Nbhs [def, in mathcomp.analysis.topology]
Builders_100.Builders_100_T__canonical__topology_Topological [def, in mathcomp.analysis.topology]
Builders_100.HB_unnamed_factory_102 [def, in mathcomp.analysis.topology]
Builders_100.topology_Pointed_isSubBaseTopological__to__topology_isFiltered [def, in mathcomp.analysis.topology]
Builders_100.topology_Pointed_isSubBaseTopological__to__topology_Nbhs_isTopological [def, in mathcomp.analysis.topology]
Builders_100.topology_Pointed_isSubBaseTopological__to__topology_selfFiltered [def, in mathcomp.analysis.topology]
Builders_14.Builders_14_T__canonical__choice_Choice [def, in mathcomp.analysis.measure]
Builders_14.Builders_14_T__canonical__classical_sets_Pointed [def, in mathcomp.analysis.measure]
Builders_14.Builders_14_T__canonical__eqtype_Equality [def, in mathcomp.analysis.measure]
Builders_14.Builders_14_T__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
Builders_14.Builders_14_T__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
Builders_14.HB_unnamed_factory_16 [def, in mathcomp.analysis.measure]
Builders_14.HB_unnamed_factory_18 [def, in mathcomp.analysis.measure]
Builders_15.Builders_15_f__canonical__functions_Inject [def, in mathcomp.classical.functions]
Builders_15.Builders_15_f__canonical__functions_Inversible [def, in mathcomp.classical.functions]
Builders_15.Builders_15_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_15.Builders_15_f__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
Builders_15.HB_unnamed_factory_17 [def, in mathcomp.classical.functions]
Builders_165.Builders_165_M__canonical__choice_Choice [def, in mathcomp.analysis.topology]
Builders_165.Builders_165_M__canonical__classical_sets_Pointed [def, in mathcomp.analysis.topology]
Builders_165.Builders_165_M__canonical__eqtype_Equality [def, in mathcomp.analysis.topology]
Builders_165.Builders_165_M__canonical__topology_Filtered [def, in mathcomp.analysis.topology]
Builders_165.Builders_165_M__canonical__topology_Nbhs [def, in mathcomp.analysis.topology]
Builders_165.Builders_165_M__canonical__topology_Topological [def, in mathcomp.analysis.topology]
Builders_165.Builders_165_M__canonical__topology_Uniform [def, in mathcomp.analysis.topology]
Builders_165.HB_unnamed_factory_167 [def, in mathcomp.analysis.topology]
Builders_165.HB_unnamed_factory_169 [def, in mathcomp.analysis.topology]
Builders_165.topology_Nbhs_isUniform__to__topology_Nbhs_isTopological [def, in mathcomp.analysis.topology]
Builders_167.Builders_167_mu__canonical__measure_Content [def, in mathcomp.analysis.measure]
Builders_167.Builders_167_mu__canonical__measure_Measure [def, in mathcomp.analysis.measure]
Builders_167.HB_unnamed_factory_169 [def, in mathcomp.analysis.measure]
Builders_172.Builders_172_M__canonical__choice_Choice [def, in mathcomp.analysis.topology]
Builders_172.Builders_172_M__canonical__classical_sets_Pointed [def, in mathcomp.analysis.topology]
Builders_172.Builders_172_M__canonical__eqtype_Equality [def, in mathcomp.analysis.topology]
Builders_172.Builders_172_M__canonical__topology_Filtered [def, in mathcomp.analysis.topology]
Builders_172.Builders_172_M__canonical__topology_Nbhs [def, in mathcomp.analysis.topology]
Builders_172.Builders_172_M__canonical__topology_Topological [def, in mathcomp.analysis.topology]
Builders_172.Builders_172_M__canonical__topology_Uniform [def, in mathcomp.analysis.topology]
Builders_172.HB_unnamed_factory_174 [def, in mathcomp.analysis.topology]
Builders_172.HB_unnamed_factory_177 [def, in mathcomp.analysis.topology]
Builders_172.topology_isUniform__to__topology_isFiltered [def, in mathcomp.analysis.topology]
Builders_172.topology_isUniform__to__topology_Nbhs_isTopological [def, in mathcomp.analysis.topology]
Builders_172.topology_isUniform__to__topology_Nbhs_isUniform_mixin [def, in mathcomp.analysis.topology]
Builders_172.topology_isUniform__to__topology_selfFiltered [def, in mathcomp.analysis.topology]
Builders_174.Builders_174_mu__canonical__measure_Content [def, in mathcomp.analysis.measure]
Builders_174.Builders_174_mu__canonical__measure_Measure [def, in mathcomp.analysis.measure]
Builders_174.Builders_174_mu__canonical__measure_SFiniteMeasure [def, in mathcomp.analysis.measure]
Builders_174.Builders_174_mu__canonical__measure_SigmaFiniteContent [def, in mathcomp.analysis.measure]
Builders_174.Builders_174_mu__canonical__measure_SigmaFiniteMeasure [def, in mathcomp.analysis.measure]
Builders_174.HB_unnamed_factory_176 [def, in mathcomp.analysis.measure]
Builders_174.HB_unnamed_factory_178 [def, in mathcomp.analysis.measure]
Builders_187.Builders_187_k__canonical__measure_Content [def, in mathcomp.analysis.measure]
Builders_187.Builders_187_k__canonical__measure_FiniteMeasure [def, in mathcomp.analysis.measure]
Builders_187.Builders_187_k__canonical__measure_FinNumFun [def, in mathcomp.analysis.measure]
Builders_187.Builders_187_k__canonical__measure_Measure [def, in mathcomp.analysis.measure]
Builders_187.Builders_187_k__canonical__measure_SFiniteMeasure [def, in mathcomp.analysis.measure]
Builders_187.Builders_187_k__canonical__measure_SigmaFiniteContent [def, in mathcomp.analysis.measure]
Builders_187.Builders_187_k__canonical__measure_SigmaFiniteMeasure [def, in mathcomp.analysis.measure]
Builders_187.HB_unnamed_factory_189 [def, in mathcomp.analysis.measure]
Builders_187.HB_unnamed_factory_191 [def, in mathcomp.analysis.measure]
Builders_187.HB_unnamed_factory_193 [def, in mathcomp.analysis.measure]
Builders_196.Builders_196_k__canonical__measure_Content [def, in mathcomp.analysis.measure]
Builders_196.Builders_196_k__canonical__measure_Measure [def, in mathcomp.analysis.measure]
Builders_196.Builders_196_k__canonical__measure_SFiniteMeasure [def, in mathcomp.analysis.measure]
Builders_196.HB_unnamed_factory_198 [def, in mathcomp.analysis.measure]
Builders_20.Builders_20_f__canonical__functions_Inversible [def, in mathcomp.classical.functions]
Builders_20.Builders_20_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_20.Builders_20_f__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
Builders_20.Builders_20_f__canonical__functions_Surject [def, in mathcomp.classical.functions]
Builders_20.HB_unnamed_factory_22 [def, in mathcomp.classical.functions]
Builders_21.Builders_21_T__canonical__choice_Choice [def, in mathcomp.analysis.measure]
Builders_21.Builders_21_T__canonical__classical_sets_Pointed [def, in mathcomp.analysis.measure]
Builders_21.Builders_21_T__canonical__eqtype_Equality [def, in mathcomp.analysis.measure]
Builders_21.Builders_21_T__canonical__measure_AlgebraOfSets [def, in mathcomp.analysis.measure]
Builders_21.Builders_21_T__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
Builders_21.Builders_21_T__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
Builders_21.HB_unnamed_factory_25 [def, in mathcomp.analysis.measure]
Builders_21.measure_isAlgebraOfSets__to__measure_isSemiRingOfSets [def, in mathcomp.analysis.measure]
Builders_21.measure_isAlgebraOfSets__to__measure_SemiRingOfSets_isRingOfSets [def, in mathcomp.analysis.measure]
Builders_21.T_isRingOfSets [def, in mathcomp.analysis.measure]
Builders_22.Builders_22_f__canonical__cardinality_FImFun [def, in mathcomp.analysis.lebesgue_integral]
Builders_22.HB_unnamed_factory_24 [def, in mathcomp.analysis.lebesgue_integral]
Builders_225.Builders_225_M__canonical__choice_Choice [def, in mathcomp.analysis.topology]
Builders_225.Builders_225_M__canonical__classical_sets_Pointed [def, in mathcomp.analysis.topology]
Builders_225.Builders_225_M__canonical__eqtype_Equality [def, in mathcomp.analysis.topology]
Builders_225.Builders_225_M__canonical__topology_Filtered [def, in mathcomp.analysis.topology]
Builders_225.Builders_225_M__canonical__topology_Nbhs [def, in mathcomp.analysis.topology]
Builders_225.Builders_225_M__canonical__topology_PseudoMetric [def, in mathcomp.analysis.topology]
Builders_225.Builders_225_M__canonical__topology_Topological [def, in mathcomp.analysis.topology]
Builders_225.Builders_225_M__canonical__topology_Uniform [def, in mathcomp.analysis.topology]
Builders_225.HB_unnamed_factory_227 [def, in mathcomp.analysis.topology]
Builders_225.HB_unnamed_factory_230 [def, in mathcomp.analysis.topology]
Builders_225.topology_Nbhs_isPseudoMetric__to__topology_Nbhs_isTopological [def, in mathcomp.analysis.topology]
Builders_225.topology_Nbhs_isPseudoMetric__to__topology_Nbhs_isUniform_mixin [def, in mathcomp.analysis.topology]
Builders_232.Builders_232_P__canonical__measure_Content [def, in mathcomp.analysis.measure]
Builders_232.Builders_232_P__canonical__measure_FiniteMeasure [def, in mathcomp.analysis.measure]
Builders_232.Builders_232_P__canonical__measure_FinNumFun [def, in mathcomp.analysis.measure]
Builders_232.Builders_232_P__canonical__measure_Measure [def, in mathcomp.analysis.measure]
Builders_232.Builders_232_P__canonical__measure_SFiniteMeasure [def, in mathcomp.analysis.measure]
Builders_232.Builders_232_P__canonical__measure_SigmaFiniteContent [def, in mathcomp.analysis.measure]
Builders_232.Builders_232_P__canonical__measure_SigmaFiniteMeasure [def, in mathcomp.analysis.measure]
Builders_232.Builders_232_P__canonical__measure_SubProbability [def, in mathcomp.analysis.measure]
Builders_232.HB_unnamed_factory_234 [def, in mathcomp.analysis.measure]
Builders_232.HB_unnamed_factory_238 [def, in mathcomp.analysis.measure]
Builders_232.measure_Measure_isSubProbability__to__measure_isFinite [def, in mathcomp.analysis.measure]
Builders_232.measure_Measure_isSubProbability__to__measure_isSFinite [def, in mathcomp.analysis.measure]
Builders_232.measure_Measure_isSubProbability__to__measure_isSigmaFinite [def, in mathcomp.analysis.measure]
Builders_247.Builders_247_P__canonical__measure_Content [def, in mathcomp.analysis.measure]
Builders_247.Builders_247_P__canonical__measure_FiniteMeasure [def, in mathcomp.analysis.measure]
Builders_247.Builders_247_P__canonical__measure_FinNumFun [def, in mathcomp.analysis.measure]
Builders_247.Builders_247_P__canonical__measure_Measure [def, in mathcomp.analysis.measure]
Builders_247.Builders_247_P__canonical__measure_Probability [def, in mathcomp.analysis.measure]
Builders_247.Builders_247_P__canonical__measure_SFiniteMeasure [def, in mathcomp.analysis.measure]
Builders_247.Builders_247_P__canonical__measure_SigmaFiniteContent [def, in mathcomp.analysis.measure]
Builders_247.Builders_247_P__canonical__measure_SigmaFiniteMeasure [def, in mathcomp.analysis.measure]
Builders_247.Builders_247_P__canonical__measure_SubProbability [def, in mathcomp.analysis.measure]
Builders_247.HB_unnamed_factory_249 [def, in mathcomp.analysis.measure]
Builders_247.HB_unnamed_factory_254 [def, in mathcomp.analysis.measure]
Builders_247.measure_Measure_isProbability__to__measure_isFinite [def, in mathcomp.analysis.measure]
Builders_247.measure_Measure_isProbability__to__measure_isSFinite [def, in mathcomp.analysis.measure]
Builders_247.measure_Measure_isProbability__to__measure_isSigmaFinite [def, in mathcomp.analysis.measure]
Builders_247.measure_Measure_isProbability__to__measure_isSubProbability [def, in mathcomp.analysis.measure]
Builders_25.HB_unnamed_factory_27 [def, in mathcomp.analysis.topology]
Builders_25.HB_unnamed_factory_29 [def, in mathcomp.analysis.topology]
Builders_28.Builders_28_f__canonical__cardinality_FImFun [def, in mathcomp.analysis.numfun]
Builders_28.Builders_28_T__canonical__choice_Choice [def, in mathcomp.analysis.measure]
Builders_28.Builders_28_T__canonical__classical_sets_Pointed [def, in mathcomp.analysis.measure]
Builders_28.Builders_28_T__canonical__eqtype_Equality [def, in mathcomp.analysis.measure]
Builders_28.Builders_28_T__canonical__measure_AlgebraOfSets [def, in mathcomp.analysis.measure]
Builders_28.Builders_28_T__canonical__measure_Measurable [def, in mathcomp.analysis.measure]
Builders_28.Builders_28_T__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
Builders_28.Builders_28_T__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
Builders_28.Builders_28_T__canonical__measure_SigmaRing [def, in mathcomp.analysis.measure]
Builders_28.HB_unnamed_factory_30 [def, in mathcomp.analysis.measure]
Builders_28.HB_unnamed_factory_30 [def, in mathcomp.analysis.numfun]
Builders_28.HB_unnamed_factory_34 [def, in mathcomp.analysis.measure]
Builders_28.measure_isMeasurable__to__measure_isSemiRingOfSets [def, in mathcomp.analysis.measure]
Builders_28.measure_isMeasurable__to__measure_RingOfSets_isAlgebraOfSets [def, in mathcomp.analysis.measure]
Builders_28.measure_isMeasurable__to__measure_SemiRingOfSets_isRingOfSets [def, in mathcomp.analysis.measure]
Builders_29.Builders_29_k__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
Builders_29.Builders_29_k__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
Builders_29.HB_unnamed_factory_31 [def, in mathcomp.analysis.kernel]
Builders_298.Builders_298_mu__canonical__measure_OuterMeasure [def, in mathcomp.analysis.measure]
Builders_298.HB_unnamed_factory_300 [def, in mathcomp.analysis.measure]
Builders_336.Builders_336_f__canonical__functions_Inversible [def, in mathcomp.classical.functions]
Builders_336.Builders_336_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_336.Builders_336_f__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
Builders_336.Builders_336_f__canonical__functions_Surject [def, in mathcomp.classical.functions]
Builders_336.functions_CanV__to__functions_OInv [def, in mathcomp.classical.functions]
Builders_336.functions_CanV__to__functions_OInv_CanV [def, in mathcomp.classical.functions]
Builders_336.functions_CanV__to__functions_OInv_Inv [def, in mathcomp.classical.functions]
Builders_336.HB_unnamed_factory_338 [def, in mathcomp.classical.functions]
Builders_336.HB_unnamed_factory_341 [def, in mathcomp.classical.functions]
Builders_344.Builders_344_f__canonical__functions_Bij [def, in mathcomp.classical.functions]
Builders_344.Builders_344_f__canonical__functions_Fun [def, in mathcomp.classical.functions]
Builders_344.Builders_344_f__canonical__functions_Inject [def, in mathcomp.classical.functions]
Builders_344.Builders_344_f__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Builders_344.Builders_344_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_344.Builders_344_f__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Builders_344.Builders_344_f__canonical__functions_Surject [def, in mathcomp.classical.functions]
Builders_344.Builders_344_f__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Builders_344.HB_unnamed_factory_346 [def, in mathcomp.classical.functions]
Builders_344.HB_unnamed_factory_348 [def, in mathcomp.classical.functions]
Builders_344.HB_unnamed_factory_350 [def, in mathcomp.classical.functions]
Builders_353.Builders_353_f__canonical__functions_Bij [def, in mathcomp.classical.functions]
Builders_353.Builders_353_f__canonical__functions_Fun [def, in mathcomp.classical.functions]
Builders_353.Builders_353_f__canonical__functions_Inject [def, in mathcomp.classical.functions]
Builders_353.Builders_353_f__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Builders_353.Builders_353_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_353.Builders_353_f__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Builders_353.Builders_353_f__canonical__functions_Surject [def, in mathcomp.classical.functions]
Builders_353.Builders_353_f__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Builders_353.functions_OCan2__to__functions_isFun [def, in mathcomp.classical.functions]
Builders_353.functions_OCan2__to__functions_OInv_Can [def, in mathcomp.classical.functions]
Builders_353.functions_OCan2__to__functions_OInv_CanV [def, in mathcomp.classical.functions]
Builders_353.HB_unnamed_factory_355 [def, in mathcomp.classical.functions]
Builders_353.HB_unnamed_factory_357 [def, in mathcomp.classical.functions]
Builders_36.Builders_36_k__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
Builders_36.Builders_36_k__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
Builders_36.Builders_36_k__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
Builders_36.Builders_36_k__canonical__kernel_SubProbabilityKernel [def, in mathcomp.analysis.kernel]
Builders_36.HB_unnamed_factory_38 [def, in mathcomp.analysis.kernel]
Builders_36.HB_unnamed_factory_41 [def, in mathcomp.analysis.kernel]
Builders_36.kernel_Kernel_isSubProbability__to__kernel_Kernel_isSFinite_subdef [def, in mathcomp.analysis.kernel]
Builders_36.kernel_Kernel_isSubProbability__to__kernel_SFiniteKernel_isFinite [def, in mathcomp.analysis.kernel]
Builders_362.Builders_362_f__canonical__functions_Inject [def, in mathcomp.classical.functions]
Builders_362.Builders_362_f__canonical__functions_Inversible [def, in mathcomp.classical.functions]
Builders_362.Builders_362_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_362.Builders_362_f__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
Builders_362.functions_Can__to__functions_OInv [def, in mathcomp.classical.functions]
Builders_362.functions_Can__to__functions_OInv_Can [def, in mathcomp.classical.functions]
Builders_362.functions_Can__to__functions_OInv_Inv [def, in mathcomp.classical.functions]
Builders_362.HB_unnamed_factory_364 [def, in mathcomp.classical.functions]
Builders_362.HB_unnamed_factory_367 [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_Bij [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_Fun [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_Inject [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_Inversible [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_InvFun [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_Surject [def, in mathcomp.classical.functions]
Builders_370.Builders_370_f__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Builders_370.functions_Inv_Can2__to__functions_OInv_Can [def, in mathcomp.classical.functions]
Builders_370.functions_Inv_Can2__to__functions_OInv_CanV [def, in mathcomp.classical.functions]
Builders_370.HB_unnamed_factory_372 [def, in mathcomp.classical.functions]
Builders_370.HB_unnamed_factory_374 [def, in mathcomp.classical.functions]
Builders_370.HB_unnamed_factory_376 [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_Bij [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_Fun [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_Inject [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_Inversible [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_InvFun [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_Surject [def, in mathcomp.classical.functions]
Builders_379.Builders_379_f__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Builders_379.functions_Can2__to__functions_isFun [def, in mathcomp.classical.functions]
Builders_379.functions_Can2__to__functions_OInv [def, in mathcomp.classical.functions]
Builders_379.functions_Can2__to__functions_OInv_Can [def, in mathcomp.classical.functions]
Builders_379.functions_Can2__to__functions_OInv_CanV [def, in mathcomp.classical.functions]
Builders_379.functions_Can2__to__functions_OInv_Inv [def, in mathcomp.classical.functions]
Builders_379.HB_unnamed_factory_381 [def, in mathcomp.classical.functions]
Builders_379.HB_unnamed_factory_384 [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_Bij [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_Fun [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_Inject [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_Inversible [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_InvFun [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_Surject [def, in mathcomp.classical.functions]
Builders_389.Builders_389_f__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Builders_389.functions_SplitInjFun_CanV__to__functions_OInv_CanV [def, in mathcomp.classical.functions]
Builders_389.HB_unnamed_factory_391 [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_Bij [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_Fun [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_Inject [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_Inversible [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_InvFun [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_Surject [def, in mathcomp.classical.functions]
Builders_394.Builders_394_f__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Builders_394.functions_BijTT__to__functions_isFun [def, in mathcomp.classical.functions]
Builders_394.functions_BijTT__to__functions_OInv [def, in mathcomp.classical.functions]
Builders_394.functions_BijTT__to__functions_OInv_Can [def, in mathcomp.classical.functions]
Builders_394.functions_BijTT__to__functions_OInv_CanV [def, in mathcomp.classical.functions]
Builders_394.functions_BijTT__to__functions_OInv_Inv [def, in mathcomp.classical.functions]
Builders_394.HB_unnamed_factory_396 [def, in mathcomp.classical.functions]
Builders_44.Builders_44_k__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
Builders_44.Builders_44_k__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
Builders_44.Builders_44_k__canonical__kernel_ProbabilityKernel [def, in mathcomp.analysis.kernel]
Builders_44.Builders_44_k__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
Builders_44.Builders_44_k__canonical__kernel_SubProbabilityKernel [def, in mathcomp.analysis.kernel]
Builders_44.HB_unnamed_factory_46 [def, in mathcomp.analysis.kernel]
Builders_44.HB_unnamed_factory_50 [def, in mathcomp.analysis.kernel]
Builders_44.kernel_Kernel_isProbability__to__kernel_FiniteKernel_isSubProbability [def, in mathcomp.analysis.kernel]
Builders_44.kernel_Kernel_isProbability__to__kernel_Kernel_isSFinite_subdef [def, in mathcomp.analysis.kernel]
Builders_44.kernel_Kernel_isProbability__to__kernel_SFiniteKernel_isFinite [def, in mathcomp.analysis.kernel]
Builders_461.Builders_461_f__canonical__functions_Inject [def, in mathcomp.classical.functions]
Builders_461.Builders_461_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_461.functions_Inj__to__functions_OInv [def, in mathcomp.classical.functions]
Builders_461.HB_unnamed_factory_463 [def, in mathcomp.classical.functions]
Builders_461.HB_unnamed_factory_465 [def, in mathcomp.classical.functions]
Builders_468.Builders_468_f__canonical__functions_Bij [def, in mathcomp.classical.functions]
Builders_468.Builders_468_f__canonical__functions_Fun [def, in mathcomp.classical.functions]
Builders_468.Builders_468_f__canonical__functions_Inject [def, in mathcomp.classical.functions]
Builders_468.Builders_468_f__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Builders_468.Builders_468_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_468.Builders_468_f__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Builders_468.Builders_468_f__canonical__functions_Surject [def, in mathcomp.classical.functions]
Builders_468.Builders_468_f__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Builders_468.Builders_468_g__canonical__functions_Inject [def, in mathcomp.classical.functions]
Builders_468.Builders_468_g__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_468.functions_Inj__to__functions_OInv [def, in mathcomp.classical.functions]
Builders_468.functions_Inj__to__functions_OInv_Can [def, in mathcomp.classical.functions]
Builders_468.HB_unnamed_factory_470 [def, in mathcomp.classical.functions]
Builders_468.HB_unnamed_factory_475 [def, in mathcomp.classical.functions]
Builders_468.HB_unnamed_mixin_473 [def, in mathcomp.classical.functions]
Builders_468.HB_unnamed_mixin_474 [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_Bij [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_Fun [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_Inject [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_InjFun [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_Inversible [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_InvFun [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_Surject [def, in mathcomp.classical.functions]
Builders_478.Builders_478_f__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
Builders_478.functions_SplitSurjFun_Inj__to__functions_OInv_Can [def, in mathcomp.classical.functions]
Builders_478.HB_unnamed_factory_480 [def, in mathcomp.classical.functions]
Builders_49.Builders_49_T__canonical__choice_Choice [def, in mathcomp.classical.classical_sets]
Builders_49.Builders_49_T__canonical__choice_Countable [def, in mathcomp.classical.classical_sets]
Builders_49.Builders_49_T__canonical__classical_sets_Empty [def, in mathcomp.classical.classical_sets]
Builders_49.Builders_49_T__canonical__eqtype_Equality [def, in mathcomp.classical.classical_sets]
Builders_49.Builders_49_T__canonical__fintype_Finite [def, in mathcomp.classical.classical_sets]
Builders_49.classical_sets_Choice_isEmpty__to__choice_Choice_isCountable [def, in mathcomp.classical.classical_sets]
Builders_49.HB_unnamed_factory_51 [def, in mathcomp.classical.classical_sets]
Builders_49.HB_unnamed_factory_53 [def, in mathcomp.classical.classical_sets]
Builders_49.HB_unnamed_factory_55 [def, in mathcomp.classical.classical_sets]
Builders_49.pickle [def, in mathcomp.classical.classical_sets]
Builders_49.unpickle [def, in mathcomp.classical.classical_sets]
Builders_5.Builders_5_k__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
Builders_5.Builders_5_k__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
Builders_5.Builders_5_k__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
Builders_5.HB_unnamed_factory_7 [def, in mathcomp.analysis.kernel]
Builders_5.HB_unnamed_factory_9 [def, in mathcomp.analysis.kernel]
Builders_58.Builders_58_T__canonical__choice_Choice [def, in mathcomp.classical.classical_sets]
Builders_58.Builders_58_T__canonical__choice_Countable [def, in mathcomp.classical.classical_sets]
Builders_58.Builders_58_T__canonical__classical_sets_Empty [def, in mathcomp.classical.classical_sets]
Builders_58.Builders_58_T__canonical__eqtype_Equality [def, in mathcomp.classical.classical_sets]
Builders_58.Builders_58_T__canonical__fintype_Finite [def, in mathcomp.classical.classical_sets]
Builders_58.classical_sets_Type_isEmpty__to__choice_Choice_isCountable [def, in mathcomp.classical.classical_sets]
Builders_58.classical_sets_Type_isEmpty__to__classical_sets_isEmpty [def, in mathcomp.classical.classical_sets]
Builders_58.classical_sets_Type_isEmpty__to__fintype_isFinite [def, in mathcomp.classical.classical_sets]
Builders_58.eq_op [def, in mathcomp.classical.classical_sets]
Builders_58.find [def, in mathcomp.classical.classical_sets]
Builders_58.HB_unnamed_factory_60 [def, in mathcomp.classical.classical_sets]
Builders_58.HB_unnamed_factory_62 [def, in mathcomp.classical.classical_sets]
Builders_58.HB_unnamed_factory_64 [def, in mathcomp.classical.classical_sets]
Builders_6.Builders_6_T__canonical__choice_Choice [def, in mathcomp.analysis.measure]
Builders_6.Builders_6_T__canonical__classical_sets_Pointed [def, in mathcomp.analysis.measure]
Builders_6.Builders_6_T__canonical__eqtype_Equality [def, in mathcomp.analysis.measure]
Builders_6.Builders_6_T__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
Builders_6.Builders_6_T__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
Builders_6.Builders_6_T__canonical__measure_SigmaRing [def, in mathcomp.analysis.measure]
Builders_6.HB_unnamed_factory_10 [def, in mathcomp.analysis.measure]
Builders_6.HB_unnamed_factory_8 [def, in mathcomp.analysis.measure]
Builders_6.measure_isSigmaRing__to__measure_SemiRingOfSets_isRingOfSets [def, in mathcomp.analysis.measure]
Builders_78.Builders_78_mu__canonical__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
Builders_78.Builders_78_mu__canonical__charge_Charge [def, in mathcomp.analysis.charge]
Builders_78.Builders_78_mu__canonical__measure_Content [def, in mathcomp.analysis.charge]
Builders_78.Builders_78_mu__canonical__measure_FinNumFun [def, in mathcomp.analysis.charge]
Builders_78.Builders_78_mu__canonical__measure_Measure [def, in mathcomp.analysis.charge]
Builders_78.HB_unnamed_factory_80 [def, in mathcomp.analysis.charge]
Builders_78.measure_Measure_isFinite__to__charge_isAdditiveCharge [def, in mathcomp.analysis.charge]
Builders_78.measure_Measure_isFinite__to__charge_isSemiSigmaAdditive [def, in mathcomp.analysis.charge]
Builders_78.measure_Measure_isFinite__to__measure_isFinite [def, in mathcomp.analysis.charge]
Builders_8.Builders_8_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
Builders_8.HB_unnamed_factory_10 [def, in mathcomp.classical.functions]
Builders_8.HB_unnamed_factory_12 [def, in mathcomp.classical.functions]
Builders_80.Builders_80_T__canonical__choice_Choice [def, in mathcomp.analysis.topology]
Builders_80.Builders_80_T__canonical__classical_sets_Pointed [def, in mathcomp.analysis.topology]
Builders_80.Builders_80_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology]
Builders_80.Builders_80_T__canonical__topology_Filtered [def, in mathcomp.analysis.topology]
Builders_80.Builders_80_T__canonical__topology_Nbhs [def, in mathcomp.analysis.topology]
Builders_80.Builders_80_T__canonical__topology_Topological [def, in mathcomp.analysis.topology]
Builders_80.HB_unnamed_factory_82 [def, in mathcomp.analysis.topology]
Builders_80.open_of_nbhs [def, in mathcomp.analysis.topology]
Builders_85.Builders_85_T__canonical__choice_Choice [def, in mathcomp.analysis.topology]
Builders_85.Builders_85_T__canonical__classical_sets_Pointed [def, in mathcomp.analysis.topology]
Builders_85.Builders_85_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology]
Builders_85.Builders_85_T__canonical__topology_Filtered [def, in mathcomp.analysis.topology]
Builders_85.Builders_85_T__canonical__topology_Nbhs [def, in mathcomp.analysis.topology]
Builders_85.Builders_85_T__canonical__topology_Topological [def, in mathcomp.analysis.topology]
Builders_85.HB_unnamed_factory_87 [def, in mathcomp.analysis.topology]
Builders_85.HB_unnamed_factory_90 [def, in mathcomp.analysis.topology]
Builders_85.topology_Pointed_isOpenTopological__to__topology_isFiltered [def, in mathcomp.analysis.topology]
Builders_85.topology_Pointed_isOpenTopological__to__topology_selfFiltered [def, in mathcomp.analysis.topology]
Builders_92.Builders_92_mu__canonical__measure_Content [def, in mathcomp.analysis.measure]
Builders_92.Builders_92_mu__canonical__measure_Measure [def, in mathcomp.analysis.measure]
Builders_92.HB_unnamed_factory_94 [def, in mathcomp.analysis.measure]
Builders_92.HB_unnamed_factory_96 [def, in mathcomp.analysis.measure]
Builders_93.Builders_93_T__canonical__choice_Choice [def, in mathcomp.analysis.topology]
Builders_93.Builders_93_T__canonical__classical_sets_Pointed [def, in mathcomp.analysis.topology]
Builders_93.Builders_93_T__canonical__eqtype_Equality [def, in mathcomp.analysis.topology]
Builders_93.Builders_93_T__canonical__topology_Filtered [def, in mathcomp.analysis.topology]
Builders_93.Builders_93_T__canonical__topology_Nbhs [def, in mathcomp.analysis.topology]
Builders_93.Builders_93_T__canonical__topology_Topological [def, in mathcomp.analysis.topology]
Builders_93.HB_unnamed_factory_95 [def, in mathcomp.analysis.topology]
Builders_93.open_from [def, in mathcomp.analysis.topology]
Builders_93.topology_Pointed_isBaseTopological__to__topology_isFiltered [def, in mathcomp.analysis.topology]
Builders_93.topology_Pointed_isBaseTopological__to__topology_Nbhs_isTopological [def, in mathcomp.analysis.topology]
Builders_93.topology_Pointed_isBaseTopological__to__topology_selfFiltered [def, in mathcomp.analysis.topology]