Files

  • mathcomp

    • Top

    'C' (Global Index)

    FilesABCDEFGHIJKLMNOPQRSTUVWXYZ_*
    DefinitionsABCDEFGHIJKLMNOPQRSTUVWXYZ_*
    LemmasABCDEFGHIJKLMNOPQRSTUVWXYZ_*
    AbbreviationsABCDEFGHIJKLMNOPQRSTUVWXYZ_*
    Global IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_*

    C

    cadd [def, in mathcomp.analysis.charge]
    Can [mod, in mathcomp.classical.functions]
    Can.axioms_ [rec, in mathcomp.classical.functions]
    Can.Can.A [var, in mathcomp.classical.functions]
    Can.Can.aT [var, in mathcomp.classical.functions]
    Can.Can.f [var, in mathcomp.classical.functions]
    Can.Can.rT [var, in mathcomp.classical.functions]
    Can.Exports [mod, in mathcomp.classical.functions]
    Can.funK [proj, in mathcomp.classical.functions]
    Can.inv [proj, in mathcomp.classical.functions]
    Can.phant_axioms [def, in mathcomp.classical.functions]
    Can.phant_Build [def, in mathcomp.classical.functions]
    Can2 [mod, in mathcomp.classical.functions]
    Can2.axioms_ [rec, in mathcomp.classical.functions]
    Can2.Can2.A [var, in mathcomp.classical.functions]
    Can2.Can2.aT [var, in mathcomp.classical.functions]
    Can2.Can2.B [var, in mathcomp.classical.functions]
    Can2.Can2.f [var, in mathcomp.classical.functions]
    Can2.Can2.rT [var, in mathcomp.classical.functions]
    Can2.Exports [mod, in mathcomp.classical.functions]
    Can2.funK [proj, in mathcomp.classical.functions]
    Can2.funS [proj, in mathcomp.classical.functions]
    Can2.inv [proj, in mathcomp.classical.functions]
    Can2.invK [proj, in mathcomp.classical.functions]
    Can2.invS [proj, in mathcomp.classical.functions]
    Can2.phant_axioms [def, in mathcomp.classical.functions]
    Can2.phant_Build [def, in mathcomp.classical.functions]
    can2_bij [prf, in mathcomp.classical.functions]
    can_countable [prf, in mathcomp.experimental_reals.discrete]
    can_surj [prf, in mathcomp.classical.functions]
    canon [prf, in mathcomp.classical.boolp]
    canonical [abbrev, in mathcomp.classical.boolp]
    canonical_ [abbrev, in mathcomp.classical.boolp]
    canonical_of [def, in mathcomp.classical.boolp]
    cantelli [prf, in mathcomp.analysis.probability]
    cantor [file, in mathcomp.analysis.cantor]
    Cantor_Bernstein [prf, in mathcomp.classical.cardinality]
    cantor_cantor_space__canonical__choice_Choice [def, in mathcomp.analysis.cantor]
    cantor_cantor_space__canonical__classical_sets_Pointed [def, in mathcomp.analysis.cantor]
    cantor_cantor_space__canonical__eqtype_Equality [def, in mathcomp.analysis.cantor]
    cantor_cantor_space__canonical__filter_Filtered [def, in mathcomp.analysis.cantor]
    cantor_cantor_space__canonical__filter_Nbhs [def, in mathcomp.analysis.cantor]
    cantor_cantor_space__canonical__filter_PointedFiltered [def, in mathcomp.analysis.cantor]
    cantor_cantor_space__canonical__filter_PointedNbhs [def, in mathcomp.analysis.cantor]
    cantor_cantor_space__canonical__topology_structure_PointedTopological [def, in mathcomp.analysis.cantor]
    cantor_cantor_space__canonical__topology_structure_Topological [def, in mathcomp.analysis.cantor]
    cantor_K'__canonical__choice_Choice [def, in mathcomp.analysis.cantor]
    cantor_K'__canonical__classical_sets_Pointed [def, in mathcomp.analysis.cantor]
    cantor_K'__canonical__eqtype_Equality [def, in mathcomp.analysis.cantor]
    cantor_like [def, in mathcomp.analysis.cantor]
    cantor_like_cantor_space [prf, in mathcomp.analysis.cantor]
    cantor_like_finite_prod [prf, in mathcomp.analysis.cantor]
    cantor_map [prf, in mathcomp.analysis.cantor]
    cantor_perfect [prf, in mathcomp.analysis.cantor]
    cantor_space [def, in mathcomp.analysis.cantor]
    cantor_space_compact [prf, in mathcomp.analysis.cantor]
    cantor_space_hausdorff [prf, in mathcomp.analysis.cantor]
    cantor_surj [prf, in mathcomp.analysis.cantor]
    cantor_surj_pt1 [prf, in mathcomp.analysis.cantor]
    cantor_surj_pt2 [prf, in mathcomp.analysis.cantor]
    cantor_surj_twop [prf, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_Bij [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_Fun [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_Inject [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_InjFun [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_Inversible [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_InvFun [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_OInversible [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_OInvFun [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_SplitBij [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_SplitInj [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_SplitInjFun [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_SplitSurj [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_SplitSurjFun [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_Surject [def, in mathcomp.analysis.cantor]
    cantor_tree_map__canonical__functions_SurjFun [def, in mathcomp.analysis.cantor]
    cantor_tree_of__canonical__choice_Choice [def, in mathcomp.analysis.cantor]
    cantor_tree_of__canonical__classical_sets_Pointed [def, in mathcomp.analysis.cantor]
    cantor_tree_of__canonical__eqtype_Equality [def, in mathcomp.analysis.cantor]
    cantor_tree_of__canonical__filter_Filtered [def, in mathcomp.analysis.cantor]
    cantor_tree_of__canonical__filter_Nbhs [def, in mathcomp.analysis.cantor]
    cantor_tree_of__canonical__filter_PointedFiltered [def, in mathcomp.analysis.cantor]
    cantor_tree_of__canonical__filter_PointedNbhs [def, in mathcomp.analysis.cantor]
    cantor_tree_of__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.cantor]
    cantor_tree_of__canonical__pseudometric_structure_PseudoPointedMetric [def, in mathcomp.analysis.cantor]
    cantor_tree_of__canonical__topology_structure_PointedTopological [def, in mathcomp.analysis.cantor]
    cantor_tree_of__canonical__topology_structure_Topological [def, in mathcomp.analysis.cantor]
    cantor_tree_of__canonical__uniform_structure_PointedUniform [def, in mathcomp.analysis.cantor]
    cantor_tree_of__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.cantor]
    cantor_zero_dimensional [prf, in mathcomp.analysis.cantor]
    CanV [mod, in mathcomp.classical.functions]
    CanV.axioms_ [rec, in mathcomp.classical.functions]
    CanV.CanV.A [var, in mathcomp.classical.functions]
    CanV.CanV.aT [var, in mathcomp.classical.functions]
    CanV.CanV.B [var, in mathcomp.classical.functions]
    CanV.CanV.f [var, in mathcomp.classical.functions]
    CanV.CanV.rT [var, in mathcomp.classical.functions]
    CanV.Exports [mod, in mathcomp.classical.functions]
    CanV.inv [proj, in mathcomp.classical.functions]
    CanV.invK [proj, in mathcomp.classical.functions]
    CanV.invS [proj, in mathcomp.classical.functions]
    CanV.phant_axioms [def, in mathcomp.classical.functions]
    CanV.phant_Build [def, in mathcomp.classical.functions]
    caratheodory_additive [prf, in mathcomp.analysis.measure]
    caratheodory_display [def, in mathcomp.analysis.measure]
    caratheodory_lim_lee [abbrev, in mathcomp.analysis.measure]
    caratheodory_lime_le [prf, in mathcomp.analysis.measure]
    caratheodory_measurable [def, in mathcomp.analysis.measure]
    caratheodory_measurable_bigcup [prf, in mathcomp.analysis.measure]
    caratheodory_measurable_bigsetU [prf, in mathcomp.analysis.measure]
    caratheodory_measurable_mu_ext [prf, in mathcomp.analysis.measure]
    caratheodory_measurable_set0 [prf, in mathcomp.analysis.measure]
    caratheodory_measurable_setC [prf, in mathcomp.analysis.measure]
    caratheodory_measurable_setD [prf, in mathcomp.analysis.measure]
    caratheodory_measurable_setI [prf, in mathcomp.analysis.measure]
    caratheodory_measurable_setU [prf, in mathcomp.analysis.measure]
    caratheodory_measurable_setU_le [prf, in mathcomp.analysis.measure]
    caratheodory_measurable_trivIset_bigcup [prf, in mathcomp.analysis.measure]
    caratheodory_measure.mu [var, in mathcomp.analysis.measure]
    caratheodory_measure.R [var, in mathcomp.analysis.measure]
    caratheodory_measure.T [var, in mathcomp.analysis.measure]
    caratheodory_measure.U [var, in mathcomp.analysis.measure]
    caratheodory_measure0 [prf, in mathcomp.analysis.measure]
    caratheodory_measure_ge0 [prf, in mathcomp.analysis.measure]
    caratheodory_measure_sigma_additive [prf, in mathcomp.analysis.measure]
    caratheodory_sigma_algebra.mu [var, in mathcomp.analysis.measure]
    caratheodory_sigma_algebra.R [var, in mathcomp.analysis.measure]
    caratheodory_sigma_algebra.T [var, in mathcomp.analysis.measure]
    caratheodory_theorem_sigma_algebra.additive_ext_lemmas.A [var, in mathcomp.analysis.measure]
    caratheodory_theorem_sigma_algebra.additive_ext_lemmas.B [var, in mathcomp.analysis.measure]
    caratheodory_theorem_sigma_algebra.additive_ext_lemmas.caratheodory_decomp [var, in mathcomp.analysis.measure]
    caratheodory_theorem_sigma_algebra.additive_ext_lemmas.caratheodory_decompIU [var, in mathcomp.analysis.measure]
    caratheodory_theorem_sigma_algebra.additive_ext_lemmas.mA [var, in mathcomp.analysis.measure]
    caratheodory_theorem_sigma_algebra.additive_ext_lemmas.mB [var, in mathcomp.analysis.measure]
    caratheodory_theorem_sigma_algebra.M [var, in mathcomp.analysis.measure]
    caratheodory_theorem_sigma_algebra.mu [var, in mathcomp.analysis.measure]
    caratheodory_theorem_sigma_algebra.R [var, in mathcomp.analysis.measure]
    caratheodory_theorem_sigma_algebra.T [var, in mathcomp.analysis.measure]
    caratheodory_type [def, in mathcomp.analysis.measure]
    card_bijP [prf, in mathcomp.classical.cardinality]
    card_eq [def, in mathcomp.classical.cardinality]
    card_eq0 [prf, in mathcomp.classical.cardinality]
    card_eq00 [prf, in mathcomp.classical.cardinality]
    card_eq_emptyl [prf, in mathcomp.classical.cardinality]
    card_eq_emptyr [prf, in mathcomp.classical.cardinality]
    card_eq_fsetP [prf, in mathcomp.classical.cardinality]
    card_eq_II [prf, in mathcomp.classical.cardinality]
    card_eq_image [prf, in mathcomp.classical.cardinality]
    card_eq_image2 [prf, in mathcomp.classical.cardinality]
    card_eq_imager [prf, in mathcomp.classical.cardinality]
    card_eq_le [prf, in mathcomp.classical.cardinality]
    card_eq_some2 [prf, in mathcomp.classical.cardinality]
    card_eq_somel [prf, in mathcomp.classical.cardinality]
    card_eq_somer [prf, in mathcomp.classical.cardinality]
    card_eq_sym [prf, in mathcomp.classical.cardinality]
    card_eq_trans [prf, in mathcomp.classical.cardinality]
    card_eql [prf, in mathcomp.classical.cardinality]
    card_eqP [prf, in mathcomp.classical.cardinality]
    card_eqPle [prf, in mathcomp.classical.cardinality]
    card_eqr [prf, in mathcomp.classical.cardinality]
    card_eqVP [prf, in mathcomp.classical.cardinality]
    card_eqxx [prf, in mathcomp.classical.cardinality]
    card_esym [prf, in mathcomp.classical.cardinality]
    card_fset_set [prf, in mathcomp.classical.cardinality]
    card_fset_sum1 [prf, in mathcomp.classical.mathcomp_extra]
    card_ge0 [prf, in mathcomp.classical.cardinality]
    card_ge_image [prf, in mathcomp.classical.cardinality]
    card_ge_preimage [prf, in mathcomp.classical.cardinality]
    card_ge_some [prf, in mathcomp.classical.cardinality]
    card_II [prf, in mathcomp.classical.cardinality]
    card_IID [prf, in mathcomp.classical.cardinality]
    card_image [prf, in mathcomp.classical.cardinality]
    card_image_le [prf, in mathcomp.classical.cardinality]
    card_imsub [prf, in mathcomp.classical.cardinality]
    card_le [def, in mathcomp.classical.cardinality]
    card_le0 [prf, in mathcomp.classical.cardinality]
    card_le0P [prf, in mathcomp.classical.cardinality]
    card_le_emptyl [prf, in mathcomp.classical.cardinality]
    card_le_emptyr [prf, in mathcomp.classical.cardinality]
    card_le_eql [prf, in mathcomp.classical.cardinality]
    card_le_eqr [prf, in mathcomp.classical.cardinality]
    card_le_finite [prf, in mathcomp.classical.cardinality]
    card_le_II [prf, in mathcomp.classical.cardinality]
    card_le_image [prf, in mathcomp.classical.cardinality]
    card_le_image2 [prf, in mathcomp.classical.cardinality]
    card_le_setD [prf, in mathcomp.classical.cardinality]
    card_le_some [prf, in mathcomp.classical.cardinality]
    card_le_some2 [prf, in mathcomp.classical.cardinality]
    card_le_trans [prf, in mathcomp.classical.cardinality]
    card_leP [prf, in mathcomp.classical.cardinality]
    card_leT [prf, in mathcomp.classical.cardinality]
    card_lexx [prf, in mathcomp.classical.cardinality]
    card_nat2 [prf, in mathcomp.classical.cardinality]
    card_rat [prf, in mathcomp.classical.cardinality]
    card_set1 [prf, in mathcomp.classical.cardinality]
    card_set_bijP [prf, in mathcomp.classical.cardinality]
    card_setT [prf, in mathcomp.classical.cardinality]
    card_setT_sym [prf, in mathcomp.classical.cardinality]
    card_some [prf, in mathcomp.classical.cardinality]
    card_subP [prf, in mathcomp.classical.cardinality]
    cardinality [file, in mathcomp.classical.cardinality]
    cardinality_f__canonical__cardinality_FImFun [def, in mathcomp.classical.cardinality]
    cardinality_fimfun__canonical__GRing_AddClosed [def, in mathcomp.classical.cardinality]
    cardinality_fimfun__canonical__GRing_Mul2Closed [def, in mathcomp.analysis.numfun]
    cardinality_fimfun__canonical__GRing_MulClosed [def, in mathcomp.analysis.numfun]
    cardinality_fimfun__canonical__GRing_OppClosed [def, in mathcomp.classical.cardinality]
    cardinality_fimfun__canonical__GRing_Semiring2Closed [def, in mathcomp.analysis.numfun]
    cardinality_fimfun__canonical__GRing_SemiringClosed [def, in mathcomp.analysis.numfun]
    cardinality_fimfun__canonical__GRing_SmulClosed [def, in mathcomp.analysis.numfun]
    cardinality_fimfun__canonical__GRing_SubringClosed [def, in mathcomp.analysis.numfun]
    cardinality_fimfun__canonical__GRing_ZmodClosed [def, in mathcomp.classical.cardinality]
    cardinality_FImFun__to__cardinality_FiniteImage [def, in mathcomp.classical.cardinality]
    cardinality_FImFun__to__cardinality_FiniteImage [def, in mathcomp.analysis.numfun]
    cardinality_FImFun__to__cardinality_FiniteImage [def, in mathcomp.analysis.lebesgue_integral]
    cardinality_FImFun__to__cardinality_FiniteImage__145 [def, in mathcomp.analysis.lebesgue_integral]
    cardinality_FImFun__to__cardinality_FiniteImage__160 [def, in mathcomp.analysis.lebesgue_integral]
    cardinality_FImFun__to__cardinality_FiniteImage__188 [def, in mathcomp.analysis.lebesgue_integral]
    cardinality_FImFun__to__cardinality_FiniteImage__26 [def, in mathcomp.analysis.numfun]
    cardinality_FImFun__to__cardinality_FiniteImage__43 [def, in mathcomp.classical.cardinality]
    cardinality_FImFun__to__cardinality_FiniteImage__48 [def, in mathcomp.classical.cardinality]
    cardMR_eq_nat [abbrev, in mathcomp.classical.cardinality]
    cardXR_eq_nat [prf, in mathcomp.classical.cardinality]
    cauchy [def, in mathcomp.analysis.topology_theory.uniform_structure]
    cauchy_ball [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    cauchy_ballP [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    cauchy_cvg [def, in mathcomp.analysis.topology_theory.uniform_structure]
    cauchy_cvgP [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    cauchy_ex [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    cauchy_exP [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    cauchy_seriesP [prf, in mathcomp.analysis.sequences]
    cauchyP [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ceil_ge [prf, in mathcomp.classical.mathcomp_extra]
    ceil_ge0 [prf, in mathcomp.classical.mathcomp_extra]
    ceil_ge_int [prf, in mathcomp.classical.mathcomp_extra]
    ceil_gt0 [prf, in mathcomp.classical.mathcomp_extra]
    ceil_gt_int [prf, in mathcomp.classical.mathcomp_extra]
    ceil_le0 [prf, in mathcomp.classical.mathcomp_extra]
    ceil_lt_int [abbrev, in mathcomp.classical.mathcomp_extra]
    ceilN [prf, in mathcomp.classical.mathcomp_extra]
    CeilTheory.R [var, in mathcomp.reals.reals]
    center [abbrev, in mathcomp.analysis.normedtype]
    center [abbrev, in mathcomp.analysis.normedtype]
    center0 [prf, in mathcomp.analysis.normedtype]
    *` [not, in mathcomp.analysis.normedtype] (no scope)
    center_radius.M [var, in mathcomp.analysis.normedtype]
    center_radius.R [var, in mathcomp.analysis.normedtype]
    center_radius_realFieldType.ball_inj_center [var, in mathcomp.analysis.normedtype]
    center_radius_realFieldType.ball_inj_radius [var, in mathcomp.analysis.normedtype]
    center_radius_realFieldType.ball_inj_radius_gt0 [var, in mathcomp.analysis.normedtype]
    center_radius_realFieldType.R [var, in mathcomp.analysis.normedtype]
    cesaro [prf, in mathcomp.analysis.sequences]
    cesaro.R [var, in mathcomp.analysis.sequences]
    cesaro_converse [prf, in mathcomp.analysis.sequences]
    cesaro_converse.cesaro_converse_off_by_one [var, in mathcomp.analysis.sequences]
    cesaro_converse.R [var, in mathcomp.analysis.sequences]
    chain [def, in mathcomp.classical.wochoice]
    chain_path [def, in mathcomp.analysis.homotopy_theory.continuous_path]
    chain_path.i [var, in mathcomp.analysis.homotopy_theory.continuous_path]
    chain_path.j [var, in mathcomp.analysis.homotopy_theory.continuous_path]
    chain_path.p [var, in mathcomp.analysis.homotopy_theory.continuous_path]
    chain_path.q [var, in mathcomp.analysis.homotopy_theory.continuous_path]
    chain_path.T [var, in mathcomp.analysis.homotopy_theory.continuous_path]
    chain_path.x [var, in mathcomp.analysis.homotopy_theory.continuous_path]
    chain_path.y [var, in mathcomp.analysis.homotopy_theory.continuous_path]
    chain_path.z [var, in mathcomp.analysis.homotopy_theory.continuous_path]
    chain_path_cts [prf, in mathcomp.analysis.homotopy_theory.continuous_path]
    chain_path_cts_point [prf, in mathcomp.analysis.homotopy_theory.continuous_path]
    chain_path_one [prf, in mathcomp.analysis.homotopy_theory.continuous_path]
    chain_path_zero [prf, in mathcomp.analysis.homotopy_theory.continuous_path]
    charge [file, in mathcomp.analysis.charge]
    Charge [mod, in mathcomp.analysis.charge]
    Charge.axioms_ [rec, in mathcomp.analysis.charge]
    Charge.charge_isAdditiveCharge_mixin [proj, in mathcomp.analysis.charge]
    Charge.charge_isSemiSigmaAdditive_mixin [proj, in mathcomp.analysis.charge]
    Charge.class [proj, in mathcomp.analysis.charge]
    Charge.Exports [mod, in mathcomp.analysis.charge]
    Charge.Exports.charge_Charge__to__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
    Charge.Exports.charge_Charge__to__measure_FinNumFun [def, in mathcomp.analysis.charge]
    Charge.Exports.charge_Charge_class__to__charge_AdditiveCharge_class [def, in mathcomp.analysis.charge]
    Charge.Exports.charge_Charge_class__to__measure_FinNumFun_class [def, in mathcomp.analysis.charge]
    Charge.measure_isFinite_mixin [proj, in mathcomp.analysis.charge]
    Charge.pack_ [def, in mathcomp.analysis.charge]
    Charge.phant_clone [def, in mathcomp.analysis.charge]
    Charge.phant_on_ [def, in mathcomp.analysis.charge]
    Charge.sort [proj, in mathcomp.analysis.charge]
    Charge.type [rec, in mathcomp.analysis.charge]
    charge0 [prf, in mathcomp.analysis.charge]
    charge_add.cadd0 [var, in mathcomp.analysis.charge]
    charge_add.cadd_finite [var, in mathcomp.analysis.charge]
    charge_add.cadd_sigma_additive [var, in mathcomp.analysis.charge]
    charge_add.d [var, in mathcomp.analysis.charge]
    charge_add.n1 [var, in mathcomp.analysis.charge]
    charge_add.n2 [var, in mathcomp.analysis.charge]
    charge_add.R [var, in mathcomp.analysis.charge]
    charge_add.T [var, in mathcomp.analysis.charge]
    charge_cadd__canonical__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
    charge_cadd__canonical__charge_Charge [def, in mathcomp.analysis.charge]
    charge_cadd__canonical__measure_FinNumFun [def, in mathcomp.analysis.charge]
    charge_charge_of_finite_measure__canonical__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
    charge_charge_of_finite_measure__canonical__charge_Charge [def, in mathcomp.analysis.charge]
    charge_charge_of_finite_measure__canonical__measure_FinNumFun [def, in mathcomp.analysis.charge]
    charge_charge_variation__canonical__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
    charge_charge_variation__canonical__charge_Charge [def, in mathcomp.analysis.charge]
    charge_charge_variation__canonical__measure_Content [def, in mathcomp.analysis.charge]
    charge_charge_variation__canonical__measure_FinNumFun [def, in mathcomp.analysis.charge]
    charge_charge_variation__canonical__measure_Measure [def, in mathcomp.analysis.charge]
    charge_crestr0__canonical__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
    charge_crestr0__canonical__charge_Charge [def, in mathcomp.analysis.charge]
    charge_crestr0__canonical__measure_FinNumFun [def, in mathcomp.analysis.charge]
    charge_crestr__canonical__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
    charge_crestr__canonical__charge_Charge [def, in mathcomp.analysis.charge]
    charge_crestr__canonical__measure_FinNumFun [def, in mathcomp.analysis.charge]
    charge_cscale__canonical__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
    charge_cscale__canonical__charge_Charge [def, in mathcomp.analysis.charge]
    charge_cscale__canonical__measure_FinNumFun [def, in mathcomp.analysis.charge]
    charge_czero__canonical__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
    charge_czero__canonical__charge_Charge [def, in mathcomp.analysis.charge]
    charge_czero__canonical__measure_FinNumFun [def, in mathcomp.analysis.charge]
    charge_induced__canonical__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
    charge_induced__canonical__charge_Charge [def, in mathcomp.analysis.charge]
    charge_induced__canonical__measure_FinNumFun [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isAdditiveCharge [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isAdditiveCharge__135 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isAdditiveCharge__145 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isAdditiveCharge__32 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isAdditiveCharge__42 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isAdditiveCharge__62 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isAdditiveCharge__72 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isSemiSigmaAdditive [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isSemiSigmaAdditive__133 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isSemiSigmaAdditive__143 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isSemiSigmaAdditive__30 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isSemiSigmaAdditive__40 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isSemiSigmaAdditive__54 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isSemiSigmaAdditive__60 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__charge_isSemiSigmaAdditive__70 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__measure_isFinite [def, in mathcomp.analysis.charge]
    charge_isCharge__to__measure_isFinite__137 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__measure_isFinite__147 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__measure_isFinite__34 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__measure_isFinite__44 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__measure_isFinite__64 [def, in mathcomp.analysis.charge]
    charge_isCharge__to__measure_isFinite__74 [def, in mathcomp.analysis.charge]
    charge_jordan_neg__canonical__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
    charge_jordan_neg__canonical__charge_Charge [def, in mathcomp.analysis.charge]
    charge_jordan_neg__canonical__measure_Content [def, in mathcomp.analysis.charge]
    charge_jordan_neg__canonical__measure_FiniteMeasure [def, in mathcomp.analysis.charge]
    charge_jordan_neg__canonical__measure_FinNumFun [def, in mathcomp.analysis.charge]
    charge_jordan_neg__canonical__measure_Measure [def, in mathcomp.analysis.charge]
    charge_jordan_neg__canonical__measure_SFiniteMeasure [def, in mathcomp.analysis.charge]
    charge_jordan_neg__canonical__measure_SigmaFiniteContent [def, in mathcomp.analysis.charge]
    charge_jordan_neg__canonical__measure_SigmaFiniteMeasure [def, in mathcomp.analysis.charge]
    charge_jordan_pos__canonical__charge_AdditiveCharge [def, in mathcomp.analysis.charge]
    charge_jordan_pos__canonical__charge_Charge [def, in mathcomp.analysis.charge]
    charge_jordan_pos__canonical__measure_Content [def, in mathcomp.analysis.charge]
    charge_jordan_pos__canonical__measure_FiniteMeasure [def, in mathcomp.analysis.charge]
    charge_jordan_pos__canonical__measure_FinNumFun [def, in mathcomp.analysis.charge]
    charge_jordan_pos__canonical__measure_Measure [def, in mathcomp.analysis.charge]
    charge_jordan_pos__canonical__measure_SFiniteMeasure [def, in mathcomp.analysis.charge]
    charge_jordan_pos__canonical__measure_SigmaFiniteContent [def, in mathcomp.analysis.charge]
    charge_jordan_pos__canonical__measure_SigmaFiniteMeasure [def, in mathcomp.analysis.charge]
    charge_lemmas.d [var, in mathcomp.analysis.charge]
    charge_lemmas.R [var, in mathcomp.analysis.charge]
    charge_lemmas.T [var, in mathcomp.analysis.charge]
    charge_lemmas_realFieldType.d [var, in mathcomp.analysis.charge]
    charge_lemmas_realFieldType.R [var, in mathcomp.analysis.charge]
    charge_lemmas_realFieldType.T [var, in mathcomp.analysis.charge]
    charge_measure_of_charge__canonical__measure_Content [def, in mathcomp.analysis.charge]
    charge_measure_of_charge__canonical__measure_Measure [def, in mathcomp.analysis.charge]
    charge_of_finite_measure [def, in mathcomp.analysis.charge]
    charge_of_finite_measure.d [var, in mathcomp.analysis.charge]
    charge_of_finite_measure.mu [var, in mathcomp.analysis.charge]
    charge_of_finite_measure.nu0 [var, in mathcomp.analysis.charge]
    charge_of_finite_measure.nu_finite [var, in mathcomp.analysis.charge]
    charge_of_finite_measure.nu_sigma_additive [var, in mathcomp.analysis.charge]
    charge_of_finite_measure.R [var, in mathcomp.analysis.charge]
    charge_of_finite_measure.T [var, in mathcomp.analysis.charge]
    charge_partition [prf, in mathcomp.analysis.charge]
    charge_restriction.crestr_finite_measure_function [var, in mathcomp.analysis.charge]
    charge_restriction.crestr_semi_additive [var, in mathcomp.analysis.charge]
    charge_restriction.crestr_semi_sigma_additive [var, in mathcomp.analysis.charge]
    charge_restriction.D [var, in mathcomp.analysis.charge]
    charge_restriction.d [var, in mathcomp.analysis.charge]
    charge_restriction.mD [var, in mathcomp.analysis.charge]
    charge_restriction.nu [var, in mathcomp.analysis.charge]
    charge_restriction.R [var, in mathcomp.analysis.charge]
    charge_restriction.T [var, in mathcomp.analysis.charge]
    charge_restriction0.crestr00 [var, in mathcomp.analysis.charge]
    charge_restriction0.crestr0_fin_num_fun [var, in mathcomp.analysis.charge]
    charge_restriction0.crestr0_sigma_additive [var, in mathcomp.analysis.charge]
    charge_restriction0.D [var, in mathcomp.analysis.charge]
    charge_restriction0.d [var, in mathcomp.analysis.charge]
    charge_restriction0.mD [var, in mathcomp.analysis.charge]
    charge_restriction0.nu [var, in mathcomp.analysis.charge]
    charge_restriction0.R [var, in mathcomp.analysis.charge]
    charge_restriction0.T [var, in mathcomp.analysis.charge]
    charge_scale.cscale0 [var, in mathcomp.analysis.charge]
    charge_scale.cscale_finite_measure_function [var, in mathcomp.analysis.charge]
    charge_scale.cscale_semi_additive [var, in mathcomp.analysis.charge]
    charge_scale.cscale_sigma_additive [var, in mathcomp.analysis.charge]
    charge_scale.d [var, in mathcomp.analysis.charge]
    charge_scale.nu [var, in mathcomp.analysis.charge]
    charge_scale.r [var, in mathcomp.analysis.charge]
    charge_scale.R [var, in mathcomp.analysis.charge]
    charge_scale.T [var, in mathcomp.analysis.charge]
    charge_semi_additive [def, in mathcomp.analysis.charge]
    charge_semi_additive2 [prf, in mathcomp.analysis.charge]
    charge_semi_additive2E [prf, in mathcomp.analysis.charge]
    charge_semi_additiveW [prf, in mathcomp.analysis.charge]
    charge_semi_sigma_additive [def, in mathcomp.analysis.charge]
    charge_variation [def, in mathcomp.analysis.charge]
    charge_variation.d [var, in mathcomp.analysis.charge]
    charge_variation.d [var, in mathcomp.analysis.charge]
    charge_variation.mu0 [var, in mathcomp.analysis.charge]
    charge_variation.mu_fin [var, in mathcomp.analysis.charge]
    charge_variation.mu_ge0 [var, in mathcomp.analysis.charge]
    charge_variation.mu_sigma_additive [var, in mathcomp.analysis.charge]
    charge_variation.N [var, in mathcomp.analysis.charge]
    charge_variation.N [var, in mathcomp.analysis.charge]
    charge_variation.nu [var, in mathcomp.analysis.charge]
    charge_variation.nu [var, in mathcomp.analysis.charge]
    charge_variation.nuPN [var, in mathcomp.analysis.charge]
    charge_variation.nuPN [var, in mathcomp.analysis.charge]
    charge_variation.P [var, in mathcomp.analysis.charge]
    charge_variation.P [var, in mathcomp.analysis.charge]
    charge_variation.R [var, in mathcomp.analysis.charge]
    charge_variation.R [var, in mathcomp.analysis.charge]
    charge_variation.T [var, in mathcomp.analysis.charge]
    charge_variation.T [var, in mathcomp.analysis.charge]
    charge_variation_continuous [prf, in mathcomp.analysis.charge]
    charge_variation_continuous.d [var, in mathcomp.analysis.charge]
    charge_variation_continuous.N [var, in mathcomp.analysis.charge]
    charge_variation_continuous.nu [var, in mathcomp.analysis.charge]
    charge_variation_continuous.nuPN [var, in mathcomp.analysis.charge]
    charge_variation_continuous.P [var, in mathcomp.analysis.charge]
    charge_variation_continuous.R [var, in mathcomp.analysis.charge]
    charge_variation_continuous.T [var, in mathcomp.analysis.charge]
    charge_zero.czero0 [var, in mathcomp.analysis.charge]
    charge_zero.czero_finite_measure_function [var, in mathcomp.analysis.charge]
    charge_zero.czero_sigma_additive [var, in mathcomp.analysis.charge]
    charge_zero.d [var, in mathcomp.analysis.charge]
    charge_zero.R [var, in mathcomp.analysis.charge]
    charge_zero.T [var, in mathcomp.analysis.charge]
    chargeD [prf, in mathcomp.analysis.charge]
    chargeDI [prf, in mathcomp.analysis.charge]
    ChargeElpiOperations [mod, in mathcomp.analysis.charge]
    chargeU [prf, in mathcomp.analysis.charge]
    chebyshev [prf, in mathcomp.analysis.probability]
    chernoff [prf, in mathcomp.analysis.probability]
    choice [prf, in mathcomp.classical.boolp]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.reals.itv]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.reals.constructive_ereal]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.experimental_reals.discrete]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.classical.filter]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.classical.classical_orders]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.classical.cardinality]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.analysis.topology_theory.weak_topology]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.analysis.topology_theory.supremum_topology]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.analysis.topology_theory.subspace_topology]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.analysis.topology_theory.quotient_topology]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.analysis.topology_theory.one_point_compactification]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.analysis.normedtype]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.analysis.lebesgue_integral]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.analysis.function_spaces]
    choice_Choice__to__choice_hasChoice [def, in mathcomp.analysis.convex]
    choice_Choice__to__choice_hasChoice__18 [def, in mathcomp.reals.constructive_ereal]
    choice_Choice__to__choice_hasChoice__218 [def, in mathcomp.analysis.function_spaces]
    choice_Choice__to__choice_hasChoice__42 [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    choice_Choice__to__choice_hasChoice__53 [def, in mathcomp.classical.filter]
    choice_Choice__to__choice_hasChoice__83 [def, in mathcomp.analysis.lebesgue_integral]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.reals.itv]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.reals.constructive_ereal]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.experimental_reals.discrete]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.classical.filter]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.classical.classical_orders]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.classical.cardinality]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.analysis.topology_theory.weak_topology]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.analysis.topology_theory.supremum_topology]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.analysis.topology_theory.subspace_topology]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.analysis.topology_theory.quotient_topology]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.analysis.topology_theory.one_point_compactification]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.analysis.normedtype]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.analysis.lebesgue_integral]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.analysis.function_spaces]
    choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.analysis.convex]
    choice_Choice__to__eqtype_hasDecEq__20 [def, in mathcomp.reals.constructive_ereal]
    choice_Choice__to__eqtype_hasDecEq__220 [def, in mathcomp.analysis.function_spaces]
    choice_Choice__to__eqtype_hasDecEq__44 [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    choice_Choice__to__eqtype_hasDecEq__55 [def, in mathcomp.classical.filter]
    choice_Choice__to__eqtype_hasDecEq__85 [def, in mathcomp.analysis.lebesgue_integral]
    choice_Countable__to__choice_Choice_isCountable [def, in mathcomp.experimental_reals.discrete]
    choice_Countable__to__choice_hasChoice [def, in mathcomp.experimental_reals.discrete]
    choice_Countable__to__eqtype_hasDecEq [def, in mathcomp.experimental_reals.discrete]
    choice_isCountable__to__choice_Choice_isCountable [def, in mathcomp.reals.constructive_ereal]
    choice_isCountable__to__choice_hasChoice [def, in mathcomp.reals.constructive_ereal]
    choice_isCountable__to__eqtype_hasDecEq [def, in mathcomp.reals.constructive_ereal]
    Choice_isEmpty [mod, in mathcomp.classical.classical_sets]
    Choice_isEmpty.axiom [proj, in mathcomp.classical.classical_sets]
    Choice_isEmpty.axioms_ [rec, in mathcomp.classical.classical_sets]
    Choice_isEmpty.Choice_isEmpty.local_mixin_choice_hasChoice [var, in mathcomp.classical.classical_sets]
    Choice_isEmpty.Choice_isEmpty.local_mixin_eqtype_hasDecEq [var, in mathcomp.classical.classical_sets]
    Choice_isEmpty.Choice_isEmpty.T [var, in mathcomp.classical.classical_sets]
    Choice_isEmpty.Choice_isEmpty_T__canonical__choice_Choice [def, in mathcomp.classical.classical_sets]
    Choice_isEmpty.Choice_isEmpty_T__canonical__eqtype_Equality [def, in mathcomp.classical.classical_sets]
    Choice_isEmpty.Exports [mod, in mathcomp.classical.classical_sets]
    Choice_isEmpty.phant_axioms [def, in mathcomp.classical.classical_sets]
    Choice_isEmpty.phant_Build [def, in mathcomp.classical.classical_sets]
    choice_pickle__canonical__functions_Fun [def, in mathcomp.classical.functions]
    choice_pickle__canonical__functions_Inject [def, in mathcomp.classical.functions]
    choice_pickle__canonical__functions_InjFun [def, in mathcomp.classical.functions]
    choice_pickle__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    choice_pickle__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
    choicePcountable [prf, in mathcomp.classical.cardinality]
    choicePpointed [prf, in mathcomp.classical.classical_sets]
    cid [abbrev, in mathcomp.classical.boolp]
    cid2 [prf, in mathcomp.classical.boolp]
    cjordan_neg [def, in mathcomp.analysis.charge]
    cjordan_negE [prf, in mathcomp.analysis.charge]
    cjordan_pos [def, in mathcomp.analysis.charge]
    cjordan_posE [prf, in mathcomp.analysis.charge]
    clamp [def, in mathcomp.experimental_reals.distr]
    Clamp.R [var, in mathcomp.experimental_reals.distr]
    clamp0 [prf, in mathcomp.experimental_reals.distr]
    clamp1 [prf, in mathcomp.experimental_reals.distr]
    clamp_id [prf, in mathcomp.experimental_reals.distr]
    clamp_in01 [prf, in mathcomp.experimental_reals.distr]
    classes.C [var, in mathcomp.analysis.measure]
    classes.D [var, in mathcomp.analysis.measure]
    classes.G [var, in mathcomp.analysis.measure]
    classes.T [var, in mathcomp.analysis.measure]
    classic [prf, in mathcomp.classical.boolp]
    classical_orders [file, in mathcomp.classical.classical_orders]
    classical_orders_big_lexi_order__canonical__choice_Choice [def, in mathcomp.classical.classical_orders]
    classical_orders_big_lexi_order__canonical__eqtype_Equality [def, in mathcomp.classical.classical_orders]
    classical_orders_big_lexi_order__canonical__Order_BPOrder [def, in mathcomp.classical.classical_orders]
    classical_orders_big_lexi_order__canonical__Order_DistrLattice [def, in mathcomp.classical.classical_orders]
    classical_orders_big_lexi_order__canonical__Order_Lattice [def, in mathcomp.classical.classical_orders]
    classical_orders_big_lexi_order__canonical__Order_POrder [def, in mathcomp.classical.classical_orders]
    classical_orders_big_lexi_order__canonical__Order_Total [def, in mathcomp.classical.classical_orders]
    classical_orders_big_lexi_order__canonical__Order_TPOrder [def, in mathcomp.classical.classical_orders]
    classical_sets [file, in mathcomp.classical.classical_sets]
    classical_sets_any__canonical__functions_Bij [def, in mathcomp.classical.functions]
    classical_sets_any__canonical__functions_Fun [def, in mathcomp.classical.functions]
    classical_sets_any__canonical__functions_Inject [def, in mathcomp.classical.functions]
    classical_sets_any__canonical__functions_InjFun [def, in mathcomp.classical.functions]
    classical_sets_any__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    classical_sets_any__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
    classical_sets_any__canonical__functions_Surject [def, in mathcomp.classical.functions]
    classical_sets_any__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_Bij [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_Fun [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_Inject [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_InjFun [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_Inversible [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_InvFun [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_Surject [def, in mathcomp.classical.functions]
    classical_sets_IIord__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_Bij [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_Fun [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_Inject [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_InjFun [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_Inversible [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_InvFun [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_Surject [def, in mathcomp.classical.functions]
    classical_sets_ordII__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
    classical_sets_Pointed__to__choice_hasChoice [def, in mathcomp.classical.filter]
    classical_sets_Pointed__to__choice_hasChoice [def, in mathcomp.analysis.topology_theory.weak_topology]
    classical_sets_Pointed__to__choice_hasChoice [def, in mathcomp.analysis.topology_theory.supremum_topology]
    classical_sets_Pointed__to__choice_hasChoice [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    classical_sets_Pointed__to__choice_hasChoice [def, in mathcomp.analysis.topology_theory.matrix_topology]
    classical_sets_Pointed__to__choice_hasChoice [def, in mathcomp.analysis.measure]
    classical_sets_Pointed__to__choice_hasChoice [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
    classical_sets_Pointed__to__choice_hasChoice [def, in mathcomp.analysis.lebesgue_measure]
    classical_sets_Pointed__to__choice_hasChoice [def, in mathcomp.analysis.function_spaces]
    classical_sets_Pointed__to__choice_hasChoice [def, in mathcomp.analysis.cantor]
    classical_sets_Pointed__to__choice_hasChoice__109 [def, in mathcomp.analysis.function_spaces]
    classical_sets_Pointed__to__choice_hasChoice__22 [def, in mathcomp.analysis.topology_theory.matrix_topology]
    classical_sets_Pointed__to__choice_hasChoice__246 [def, in mathcomp.analysis.function_spaces]
    classical_sets_Pointed__to__choice_hasChoice__255 [def, in mathcomp.analysis.function_spaces]
    classical_sets_Pointed__to__choice_hasChoice__26 [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    classical_sets_Pointed__to__choice_hasChoice__28 [def, in mathcomp.analysis.topology_theory.weak_topology]
    classical_sets_Pointed__to__choice_hasChoice__341 [def, in mathcomp.analysis.measure]
    classical_sets_Pointed__to__choice_hasChoice__38 [def, in mathcomp.analysis.cantor]
    classical_sets_Pointed__to__choice_hasChoice__387 [def, in mathcomp.analysis.measure]
    classical_sets_Pointed__to__choice_hasChoice__52 [def, in mathcomp.analysis.topology_theory.matrix_topology]
    classical_sets_Pointed__to__choice_hasChoice__63 [def, in mathcomp.classical.filter]
    classical_sets_Pointed__to__choice_hasChoice__69 [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    classical_sets_Pointed__to__choice_hasChoice__93 [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.classical.filter]
    classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis_stdlib.Rstruct_topology]
    classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis.topology_theory.weak_topology]
    classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis.topology_theory.supremum_topology]
    classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis.topology_theory.one_point_compactification]
    classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis.topology_theory.matrix_topology]
    classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis.normedtype]
    classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis.measure]
    classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
    classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis.lebesgue_measure]
    classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis.function_spaces]
    classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis.cantor]
    classical_sets_Pointed__to__classical_sets_isPointed__107 [def, in mathcomp.analysis.function_spaces]
    classical_sets_Pointed__to__classical_sets_isPointed__20 [def, in mathcomp.analysis.topology_theory.matrix_topology]
    classical_sets_Pointed__to__classical_sets_isPointed__24 [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    classical_sets_Pointed__to__classical_sets_isPointed__244 [def, in mathcomp.analysis.function_spaces]
    classical_sets_Pointed__to__classical_sets_isPointed__253 [def, in mathcomp.analysis.function_spaces]
    classical_sets_Pointed__to__classical_sets_isPointed__26 [def, in mathcomp.analysis.topology_theory.weak_topology]
    classical_sets_Pointed__to__classical_sets_isPointed__339 [def, in mathcomp.analysis.measure]
    classical_sets_Pointed__to__classical_sets_isPointed__36 [def, in mathcomp.analysis.cantor]
    classical_sets_Pointed__to__classical_sets_isPointed__385 [def, in mathcomp.analysis.measure]
    classical_sets_Pointed__to__classical_sets_isPointed__50 [def, in mathcomp.analysis.topology_theory.matrix_topology]
    classical_sets_Pointed__to__classical_sets_isPointed__61 [def, in mathcomp.classical.filter]
    classical_sets_Pointed__to__classical_sets_isPointed__67 [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    classical_sets_Pointed__to__classical_sets_isPointed__91 [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    classical_sets_Pointed__to__eqtype_hasDecEq [def, in mathcomp.classical.filter]
    classical_sets_Pointed__to__eqtype_hasDecEq [def, in mathcomp.analysis.topology_theory.weak_topology]
    classical_sets_Pointed__to__eqtype_hasDecEq [def, in mathcomp.analysis.topology_theory.supremum_topology]
    classical_sets_Pointed__to__eqtype_hasDecEq [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    classical_sets_Pointed__to__eqtype_hasDecEq [def, in mathcomp.analysis.topology_theory.matrix_topology]
    classical_sets_Pointed__to__eqtype_hasDecEq [def, in mathcomp.analysis.measure]
    classical_sets_Pointed__to__eqtype_hasDecEq [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
    classical_sets_Pointed__to__eqtype_hasDecEq [def, in mathcomp.analysis.lebesgue_measure]
    classical_sets_Pointed__to__eqtype_hasDecEq [def, in mathcomp.analysis.function_spaces]
    classical_sets_Pointed__to__eqtype_hasDecEq [def, in mathcomp.analysis.cantor]
    classical_sets_Pointed__to__eqtype_hasDecEq__111 [def, in mathcomp.analysis.function_spaces]
    classical_sets_Pointed__to__eqtype_hasDecEq__24 [def, in mathcomp.analysis.topology_theory.matrix_topology]
    classical_sets_Pointed__to__eqtype_hasDecEq__248 [def, in mathcomp.analysis.function_spaces]
    classical_sets_Pointed__to__eqtype_hasDecEq__257 [def, in mathcomp.analysis.function_spaces]
    classical_sets_Pointed__to__eqtype_hasDecEq__28 [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    classical_sets_Pointed__to__eqtype_hasDecEq__30 [def, in mathcomp.analysis.topology_theory.weak_topology]
    classical_sets_Pointed__to__eqtype_hasDecEq__343 [def, in mathcomp.analysis.measure]
    classical_sets_Pointed__to__eqtype_hasDecEq__389 [def, in mathcomp.analysis.measure]
    classical_sets_Pointed__to__eqtype_hasDecEq__40 [def, in mathcomp.analysis.cantor]
    classical_sets_Pointed__to__eqtype_hasDecEq__54 [def, in mathcomp.analysis.topology_theory.matrix_topology]
    classical_sets_Pointed__to__eqtype_hasDecEq__65 [def, in mathcomp.classical.filter]
    classical_sets_Pointed__to__eqtype_hasDecEq__71 [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    classical_sets_Pointed__to__eqtype_hasDecEq__95 [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    classical_sets_set0fun__canonical__functions_Fun [def, in mathcomp.classical.functions]
    classical_sets_set0fun__canonical__functions_Inject [def, in mathcomp.classical.functions]
    classical_sets_set0fun__canonical__functions_InjFun [def, in mathcomp.classical.functions]
    classical_sets_set0fun__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    classical_sets_set0fun__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
    classical_sets_set_type__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.subtype_topology]
    classical_sets_set_type__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.subtype_topology]
    classical_sets_set_type__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.subtype_topology]
    classical_sets_set_type__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.subtype_topology]
    classical_sets_set_type__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.subtype_topology]
    classical_sets_set_type__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.subtype_topology]
    classical_sets_set_type__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.subtype_topology]
    classical_sets_setI__canonical__Monoid_AddLaw [def, in mathcomp.classical.classical_sets]
    classical_sets_setI__canonical__Monoid_ComLaw [def, in mathcomp.classical.classical_sets]
    classical_sets_setI__canonical__Monoid_Law [def, in mathcomp.classical.classical_sets]
    classical_sets_setI__canonical__Monoid_MulLaw [def, in mathcomp.classical.classical_sets]
    classical_sets_setI__canonical__SemiGroup_ComLaw [def, in mathcomp.classical.classical_sets]
    classical_sets_setI__canonical__SemiGroup_Law [def, in mathcomp.classical.classical_sets]
    classical_sets_setU__canonical__Monoid_AddLaw [def, in mathcomp.classical.classical_sets]
    classical_sets_setU__canonical__Monoid_ComLaw [def, in mathcomp.classical.classical_sets]
    classical_sets_setU__canonical__Monoid_Law [def, in mathcomp.classical.classical_sets]
    classical_sets_setU__canonical__Monoid_MulLaw [def, in mathcomp.classical.classical_sets]
    classical_sets_setU__canonical__SemiGroup_ComLaw [def, in mathcomp.classical.classical_sets]
    classical_sets_setU__canonical__SemiGroup_Law [def, in mathcomp.classical.classical_sets]
    classical_sets_setY__canonical__Monoid_AddLaw [def, in mathcomp.classical.classical_sets]
    classical_sets_setY__canonical__Monoid_ComLaw [def, in mathcomp.classical.classical_sets]
    classical_sets_setY__canonical__Monoid_Law [def, in mathcomp.classical.classical_sets]
    classical_sets_setY__canonical__SemiGroup_ComLaw [def, in mathcomp.classical.classical_sets]
    classical_sets_setY__canonical__SemiGroup_Law [def, in mathcomp.classical.classical_sets]
    classical_sets_squash__canonical__functions_Inversible [def, in mathcomp.classical.functions]
    classical_sets_squash__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    classical_sets_squash__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
    classical_sets_squash__canonical__functions_Surject [def, in mathcomp.classical.functions]
    classical_sets_Type_isEmpty__to__choice_Choice_isCountable [def, in mathcomp.classical.classical_sets]
    classical_sets_Type_isEmpty__to__choice_hasChoice [def, in mathcomp.classical.classical_sets]
    classical_sets_Type_isEmpty__to__classical_sets_isEmpty [def, in mathcomp.classical.classical_sets]
    classical_sets_Type_isEmpty__to__eqtype_hasDecEq [def, in mathcomp.classical.classical_sets]
    classical_sets_Type_isEmpty__to__fintype_isFinite [def, in mathcomp.classical.classical_sets]
    classical_sets_unsquash__canonical__functions_Inject [def, in mathcomp.classical.functions]
    classical_sets_unsquash__canonical__functions_Inversible [def, in mathcomp.classical.functions]
    classical_sets_unsquash__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    classical_sets_unsquash__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
    classicType [def, in mathcomp.classical.boolp]
    classicType.T [var, in mathcomp.classical.boolp]
    clopen [def, in mathcomp.analysis.topology_theory.topology_structure]
    clopen0 [prf, in mathcomp.analysis.topology_theory.topology_structure]
    clopen_bigcup_clopen [prf, in mathcomp.analysis.topology_theory.order_topology]
    clopen_comp [prf, in mathcomp.analysis.topology_theory.topology_structure]
    clopen_connectedP [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    clopen_countable [prf, in mathcomp.analysis.topology_theory.compact]
    clopen_separatedP [prf, in mathcomp.analysis.topology_theory.connected]
    clopen_surj [prf, in mathcomp.analysis.topology_theory.compact]
    clopenC [prf, in mathcomp.analysis.topology_theory.topology_structure]
    clopenI [prf, in mathcomp.analysis.topology_theory.topology_structure]
    clopenT [prf, in mathcomp.analysis.topology_theory.topology_structure]
    clopenU [prf, in mathcomp.analysis.topology_theory.topology_structure]
    close [def, in mathcomp.analysis.separation_axioms]
    close_cvg [prf, in mathcomp.analysis.separation_axioms]
    close_cvgxx [prf, in mathcomp.analysis.separation_axioms]
    close_eq [prf, in mathcomp.analysis.separation_axioms]
    close_refl [prf, in mathcomp.analysis.separation_axioms]
    close_sym [prf, in mathcomp.analysis.separation_axioms]
    close_trans [prf, in mathcomp.analysis.separation_axioms]
    closed [def, in mathcomp.analysis.topology_theory.topology_structure]
    Closed.T [var, in mathcomp.analysis.topology_theory.topology_structure]
    closed0 [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closed_ball [def, in mathcomp.analysis.normedtype]
    closed_ball0 [prf, in mathcomp.analysis.normedtype]
    closed_ball_ [def, in mathcomp.analysis.normedtype]
    closed_ball_ball [prf, in mathcomp.analysis.normedtype]
    closed_ball_closed [prf, in mathcomp.analysis.normedtype]
    closed_ball_itv [prf, in mathcomp.analysis.normedtype]
    closed_ball_subset [prf, in mathcomp.analysis.normedtype]
    closed_ballE [prf, in mathcomp.analysis.normedtype]
    closed_ballR_compact [prf, in mathcomp.analysis.normedtype]
    closed_ballxx [prf, in mathcomp.analysis.normedtype]
    closed_bigcup [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closed_bigI [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closed_bigsetU [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closed_closed_ball_ [prf, in mathcomp.analysis.normedtype]
    closed_closure [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closed_comp [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closed_cvg [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closed_disjoint_closed_ball [prf, in mathcomp.analysis.normedtype]
    closed_eq [prf, in mathcomp.analysis.normedtype]
    closed_ereal_ge_ereal [prf, in mathcomp.analysis.normedtype]
    closed_ereal_le_ereal [prf, in mathcomp.analysis.normedtype]
    closed_fam_of [def, in mathcomp.analysis.topology_theory.compact]
    closed_ge [prf, in mathcomp.analysis.normedtype]
    closed_le [prf, in mathcomp.analysis.normedtype]
    closed_measurable [prf, in mathcomp.analysis.lebesgue_measure]
    closed_openC [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closed_setIS [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    closed_setSI [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    closed_subspaceP [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    closed_subspaceT [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    closed_subspaceW [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    closedC [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closedE [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closedI [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closedN [prf, in mathcomp.analysis.normedtype]
    closedT [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closedU [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closeE [prf, in mathcomp.analysis.separation_axioms]
    closeEnbhs [prf, in mathcomp.analysis.separation_axioms]
    closeEonbhs [prf, in mathcomp.analysis.separation_axioms]
    closure [def, in mathcomp.analysis.topology_theory.topology_structure]
    closure0 [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closure_ball [prf, in mathcomp.analysis.normedtype]
    closure_eq0 [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closure_gt [prf, in mathcomp.analysis.normedtype]
    closure_id [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closure_interior_idem [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closure_interior_lemmas.T [var, in mathcomp.analysis.topology_theory.topology_structure]
    closure_left_right_open.R [var, in mathcomp.analysis.normedtype]
    closure_lemmas.T [var, in mathcomp.analysis.topology_theory.topology_structure]
    closure_limit_point [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closure_lt [prf, in mathcomp.analysis.normedtype]
    closure_open_regclosed [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closure_setC [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closure_subset [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closure_subspaceW [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    closure_sup [prf, in mathcomp.analysis.normedtype]
    closureC [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    closureC_deprecated [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closureE [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closureEbigcap [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closureEcluster [prf, in mathcomp.analysis.topology_theory.compact]
    closureEcvg [prf, in mathcomp.analysis.topology_theory.compact]
    closureEnbhs [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closureEonbhs [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closureI [prf, in mathcomp.analysis.topology_theory.topology_structure]
    closureU [prf, in mathcomp.analysis.topology_theory.topology_structure]
    cluster [def, in mathcomp.analysis.topology_theory.compact]
    cluster_cvgE [prf, in mathcomp.analysis.topology_theory.compact]
    cluster_nbhs [prf, in mathcomp.analysis.topology_theory.compact]
    clusterE [prf, in mathcomp.analysis.topology_theory.compact]
    clusterEonbhs [prf, in mathcomp.analysis.topology_theory.compact]
    cmp0 [prf, in mathcomp.reals.signed]
    code [def, in mathcomp.reals.constructive_ereal]
    codeK [prf, in mathcomp.reals.constructive_ereal]
    comp_can_subproof [prf, in mathcomp.classical.functions]
    comp_centerK [prf, in mathcomp.analysis.normedtype]
    comp_fimfun_subproof [prf, in mathcomp.classical.cardinality]
    comp_fun_subproof [prf, in mathcomp.classical.functions]
    comp_patch [prf, in mathcomp.classical.functions]
    comp_preimage [prf, in mathcomp.classical.classical_sets]
    comp_shiftK [prf, in mathcomp.analysis.normedtype]
    comp_surj_subproof [prf, in mathcomp.classical.functions]
    compact [file, in mathcomp.analysis.topology_theory.compact]
    compact [def, in mathcomp.analysis.topology_theory.compact]
    Compact.T [var, in mathcomp.analysis.topology_theory.compact]
    compact0 [prf, in mathcomp.analysis.topology_theory.compact]
    compact_bounded [prf, in mathcomp.analysis.normedtype]
    compact_cauchy_cvg [prf, in mathcomp.analysis.topology_theory.compact]
    compact_closed [prf, in mathcomp.analysis.separation_axioms]
    compact_closedI [prf, in mathcomp.analysis.topology_theory.compact]
    compact_cluster_set1 [prf, in mathcomp.analysis.separation_axioms]
    compact_cover [prf, in mathcomp.analysis.topology_theory.compact]
    compact_cvg_within_compact [prf, in mathcomp.analysis.function_spaces]
    compact_equicontinuous [prf, in mathcomp.analysis.function_spaces]
    compact_finite_measure [prf, in mathcomp.analysis.lebesgue_integral]
    compact_In0 [prf, in mathcomp.analysis.topology_theory.compact]
    compact_measurable [prf, in mathcomp.analysis.lebesgue_measure]
    compact_near [def, in mathcomp.analysis.topology_theory.compact]
    compact_near_coveringP [prf, in mathcomp.analysis.topology_theory.compact]
    compact_normal [prf, in mathcomp.analysis.separation_axioms]
    compact_normal_local [prf, in mathcomp.analysis.separation_axioms]
    compact_open [def, in mathcomp.analysis.function_spaces]
    compact_open.compact_open_setwise.K [var, in mathcomp.analysis.function_spaces]
    compact_open.T [var, in mathcomp.analysis.function_spaces]
    compact_open.U [var, in mathcomp.analysis.function_spaces]
    compact_open_cvgP [prf, in mathcomp.analysis.function_spaces]
    compact_open_def [def, in mathcomp.analysis.function_spaces]
    compact_open_fam_compactP [prf, in mathcomp.analysis.function_spaces]
    compact_open_of_nbhs [def, in mathcomp.analysis.function_spaces]
    compact_open_open [prf, in mathcomp.analysis.function_spaces]
    compact_open_uniform.small_ent_sub [var, in mathcomp.analysis.function_spaces]
    compact_open_uniform.U [var, in mathcomp.analysis.function_spaces]
    compact_open_uniform.V [var, in mathcomp.analysis.function_spaces]
    compact_openK [def, in mathcomp.analysis.function_spaces]
    compact_openK_nbhs [def, in mathcomp.analysis.function_spaces]
    compact_openK_nbhs_filter [inst, in mathcomp.analysis.function_spaces]
    compact_openK_nbhsE_subproof [prf, in mathcomp.analysis.function_spaces]
    compact_openK_openE_subproof [prf, in mathcomp.analysis.function_spaces]
    compact_precompact [prf, in mathcomp.analysis.separation_axioms]
    compact_regular [prf, in mathcomp.analysis.separation_axioms]
    compact_second_countable [prf, in mathcomp.analysis.topology_theory.compact]
    compact_set1 [prf, in mathcomp.analysis.topology_theory.compact]
    compact_setM [abbrev, in mathcomp.analysis.topology_theory.product_topology]
    compact_setX [prf, in mathcomp.analysis.topology_theory.product_topology]
    compact_subspaceIP [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    compact_ultra [prf, in mathcomp.analysis.topology_theory.compact]
    compactly_in [def, in mathcomp.analysis.function_spaces]
    compactU [prf, in mathcomp.analysis.topology_theory.compact]
    compE [prf, in mathcomp.classical.functions]
    Complete [mod, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.axioms_ [rec, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.choice_hasChoice_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.class [proj, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.classical_sets_isPointed_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports [mod, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete__to__choice_Choice [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete__to__classical_sets_Pointed [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete__to__filter_PointedFiltered [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete__to__filter_PointedNbhs [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete__to__topology_structure_PointedTopological [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete__to__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete__to__uniform_structure_PointedUniform [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete__to__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete_class__to__classical_sets_Pointed_class [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete_class__to__filter_PointedFiltered_class [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete_class__to__filter_PointedNbhs_class [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete_class__to__topology_structure_PointedTopological_class [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete_class__to__uniform_structure_PointedUniform_class [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.Exports.uniform_structure_Complete_class__to__uniform_structure_Uniform_class [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.filter_isFiltered_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.filter_selfFiltered_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.pack_ [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.phant_clone [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.phant_on_ [def, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.sort [proj, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.type [rec, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.uniform_structure_Nbhs_isUniform_mixin_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
    Complete.uniform_structure_Uniform_isComplete_mixin [proj, in mathcomp.analysis.topology_theory.uniform_structure]
    complete_ax [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
    completed_algebra_caratheodory.calgebra_sub_cara [var, in mathcomp.analysis.lebesgue_measure]
    completed_algebra_caratheodory.cara_sub_calgebra [var, in mathcomp.analysis.lebesgue_measure]
    completed_algebra_caratheodory.R [var, in mathcomp.analysis.lebesgue_measure]
    completed_algebra_gen [def, in mathcomp.analysis.lebesgue_measure]
    completed_caratheodory_measurable [prf, in mathcomp.analysis.lebesgue_measure]
    completed_lebesgue_measure [def, in mathcomp.analysis.lebesgue_measure]
    completed_lebesgue_measure_is_complete [prf, in mathcomp.analysis.lebesgue_measure]
    completed_lebesgue_stieltjes_measure [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
    completed_lebesgue_stieltjes_measure.hb_instance_31.f [var, in mathcomp.analysis.lebesgue_stieltjes_measure]
    completed_lebesgue_stieltjes_measure.hb_instance_39.f [var, in mathcomp.analysis.lebesgue_stieltjes_measure]
    completed_lebesgue_stieltjes_measure.R [var, in mathcomp.analysis.lebesgue_stieltjes_measure]
    completed_lebesgue_stieltjes_measure.sigmaT_finite_completed_lebesgue_stieltjes_measure [var, in mathcomp.analysis.lebesgue_stieltjes_measure]
    completed_measure_extension [def, in mathcomp.analysis.measure]
    completed_measure_extension.d [var, in mathcomp.analysis.measure]
    completed_measure_extension.I [var, in mathcomp.analysis.measure]
    completed_measure_extension.measure0 [var, in mathcomp.analysis.measure]
    completed_measure_extension.measure_ge0 [var, in mathcomp.analysis.measure]
    completed_measure_extension.measure_semi_sigma_additive [var, in mathcomp.analysis.measure]
    completed_measure_extension.mu [var, in mathcomp.analysis.measure]
    completed_measure_extension.R [var, in mathcomp.analysis.measure]
    completed_measure_extension.Rmu [var, in mathcomp.analysis.measure]
    completed_measure_extension.T [var, in mathcomp.analysis.measure]
    completed_measure_extension_sigma_finite [prf, in mathcomp.analysis.measure]
    completed_mu [abbrev, in mathcomp.analysis.lebesgue_measure]
    CompleteElpiOperations [mod, in mathcomp.analysis.topology_theory.uniform_structure]
    completely_regular.R [var, in mathcomp.analysis.normedtype]
    completely_regular_regular [prf, in mathcomp.analysis.normedtype]
    completely_regular_space [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity [mod, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.completely_regular_uniformity.completely_regular_nbhsE [var, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.completely_regular_uniformity.crs [var, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.completely_regular_uniformity.R [var, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.completely_regular_uniformity.X [var, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.completely_regular_uniformity.X' [var, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.completely_regular_uniformity_type__canonical__choice_Choice [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.completely_regular_uniformity_type__canonical__eqtype_Equality [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.completely_regular_uniformity_type__canonical__filter_Filtered [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.completely_regular_uniformity_type__canonical__filter_Nbhs [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.completely_regular_uniformity_type__canonical__topology_structure_Topological [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.completely_regular_uniformity_type__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.Exports [mod, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.HB_unnamed_factory_619 [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.HB_unnamed_factory_630 [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.HB_unnamed_factory_634 [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.HB_unnamed_mixin_625 [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.HB_unnamed_mixin_626 [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.HB_unnamed_mixin_627 [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.HB_unnamed_mixin_628 [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.HB_unnamed_mixin_629 [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.HB_unnamed_mixin_633 [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.topology_structure_Topological__to__choice_hasChoice [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.topology_structure_Topological__to__eqtype_hasDecEq [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.topology_structure_Topological__to__filter_isFiltered [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.topology_structure_Topological__to__filter_selfFiltered [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.topology_structure_Topological__to__topology_structure_Nbhs_isTopological [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.type [def, in mathcomp.analysis.normedtype]
    completely_regular_uniformity.uniform_structure_Nbhs_isUniform__to__uniform_structure_Nbhs_isUniform_mixin [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule [mod, in mathcomp.analysis.normedtype]
    CompleteNormedModule.axioms_ [rec, in mathcomp.analysis.normedtype]
    CompleteNormedModule.choice_hasChoice_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.class [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.classical_sets_isPointed_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports [mod, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_GRing_Lmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_GRing_Nmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_GRing_Zmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_normedtype_NormedModule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_normedtype_PseudoMetricNormedZmod [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_Num_NormedZmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_NbhsLmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_NbhsNmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_NbhsZmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_TopologicalLmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_TopologicalNmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_TopologicalZmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_Tvs [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_UniformLmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_pseudometric_structure_CompletePseudoMetric_and_tvs_UniformZmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_GRing_Lmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_GRing_Nmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_GRing_Zmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_normedtype_NormedModule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_normedtype_PseudoMetricNormedZmod [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_Num_NormedZmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_NbhsLmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_NbhsNmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_NbhsZmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_TopologicalLmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_TopologicalNmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_TopologicalZmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_Tvs [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_UniformLmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.join_normedtype_CompleteNormedModule_between_uniform_structure_Complete_and_tvs_UniformZmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__choice_Choice [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__classical_sets_Pointed [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__eqtype_Equality [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__filter_Filtered [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__filter_Nbhs [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__filter_PointedFiltered [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__filter_PointedNbhs [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__GRing_Lmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__GRing_Nmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__GRing_Zmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__normedtype_NormedModule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__normedtype_PseudoMetricNormedZmod [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__Num_NormedZmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__pseudometric_structure_CompletePseudoMetric [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__pseudometric_structure_PseudoPointedMetric [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__topology_structure_PointedTopological [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__topology_structure_Topological [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__tvs_NbhsLmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__tvs_NbhsNmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__tvs_NbhsZmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__tvs_TopologicalLmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__tvs_TopologicalNmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__tvs_TopologicalZmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__tvs_Tvs [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__tvs_UniformLmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__tvs_UniformZmodule [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__uniform_structure_Complete [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__uniform_structure_PointedUniform [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule__to__uniform_structure_Uniform [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__choice_Choice_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__classical_sets_Pointed_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__eqtype_Equality_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__filter_Filtered_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__filter_Nbhs_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__filter_PointedFiltered_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__filter_PointedNbhs_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__GRing_Lmodule_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__GRing_Nmodule_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__GRing_Zmodule_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__normedtype_NormedModule_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__normedtype_PseudoMetricNormedZmod_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__Num_NormedZmodule_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__pseudometric_structure_CompletePseudoMetric_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__pseudometric_structure_PseudoMetric_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__pseudometric_structure_PseudoPointedMetric_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__topology_structure_PointedTopological_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__tvs_NbhsLmodule_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__tvs_NbhsNmodule_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__tvs_NbhsZmodule_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__tvs_TopologicalLmodule_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__tvs_TopologicalNmodule_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__tvs_TopologicalZmodule_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__tvs_Tvs_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__tvs_UniformLmodule_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__tvs_UniformZmodule_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__uniform_structure_Complete_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__uniform_structure_PointedUniform_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Exports.normedtype_CompleteNormedModule_class__to__uniform_structure_Uniform_class [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.filter_isFiltered_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.filter_selfFiltered_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.GRing_isNmodule_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.GRing_Nmodule_isZmodule_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.GRing_Zmodule_isLmodule_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.normedtype_NormedZmod_PseudoMetric_eq_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.normedtype_PseudoMetricNormedZmod_Tvs_isNormedModule_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.Num_Zmodule_isNormed_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.pack_ [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.phant_clone [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.phant_on_ [def, in mathcomp.analysis.normedtype]
    CompleteNormedModule.pseudometric_structure_Uniform_isPseudoMetric_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.sort [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.tvs_Uniform_isTvs_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.type [rec, in mathcomp.analysis.normedtype]
    CompleteNormedModule.uniform_structure_Nbhs_isUniform_mixin_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModule.uniform_structure_Uniform_isComplete_mixin [proj, in mathcomp.analysis.normedtype]
    CompleteNormedModuleElpiOperations [mod, in mathcomp.analysis.normedtype]
    CompletePseudoMetric [mod, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.axioms_ [rec, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.choice_hasChoice_mixin [proj, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.class [proj, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.classical_sets_isPointed_mixin [proj, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports [mod, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.join_pseudometric_structure_CompletePseudoMetric_between_uniform_structure_Complete_and_pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.join_pseudometric_structure_CompletePseudoMetric_between_uniform_structure_Complete_and_pseudometric_structure_PseudoPointedMetric [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__choice_Choice [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__classical_sets_Pointed [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__eqtype_Equality [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__filter_Filtered [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__filter_Nbhs [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__filter_PointedFiltered [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__filter_PointedNbhs [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__pseudometric_structure_PseudoPointedMetric [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__topology_structure_PointedTopological [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__uniform_structure_Complete [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__uniform_structure_PointedUniform [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric__to__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__choice_Choice_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__classical_sets_Pointed_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__eqtype_Equality_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__filter_Filtered_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__filter_Nbhs_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__filter_PointedFiltered_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__filter_PointedNbhs_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__pseudometric_structure_PseudoMetric_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__pseudometric_structure_PseudoPointedMetric_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__topology_structure_PointedTopological_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__topology_structure_Topological_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__uniform_structure_Complete_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__uniform_structure_PointedUniform_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.Exports.pseudometric_structure_CompletePseudoMetric_class__to__uniform_structure_Uniform_class [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.filter_isFiltered_mixin [proj, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.filter_selfFiltered_mixin [proj, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.pack_ [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.phant_clone [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.phant_on_ [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.pseudometric_structure_Uniform_isPseudoMetric_mixin [proj, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.sort [proj, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.type [rec, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.uniform_structure_Nbhs_isUniform_mixin_mixin [proj, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetric.uniform_structure_Uniform_isComplete_mixin [proj, in mathcomp.analysis.topology_theory.pseudometric_structure]
    CompletePseudoMetricElpiOperations [mod, in mathcomp.analysis.topology_theory.pseudometric_structure]
    completeType1.T [var, in mathcomp.analysis.topology_theory.uniform_structure]
    component_closed [prf, in mathcomp.analysis.topology_theory.connected]
    component_connected [prf, in mathcomp.analysis.topology_theory.connected]
    compOo_eqo [prf, in mathcomp.analysis.derive]
    compoO_eqo [prf, in mathcomp.analysis.derive]
    compOo_eqox [prf, in mathcomp.analysis.derive]
    compoO_eqox [prf, in mathcomp.analysis.derive]
    compose_continuous [prf, in mathcomp.analysis.function_spaces]
    Composition.A [var, in mathcomp.classical.functions]
    Composition.A [var, in mathcomp.classical.functions]
    Composition.aT [var, in mathcomp.classical.functions]
    Composition.aT [var, in mathcomp.classical.functions]
    Composition.B [var, in mathcomp.classical.functions]
    Composition.B [var, in mathcomp.classical.functions]
    Composition.C [var, in mathcomp.classical.functions]
    Composition.C [var, in mathcomp.classical.functions]
    Composition.hb_instance_161.f [var, in mathcomp.classical.functions]
    Composition.hb_instance_161.g [var, in mathcomp.classical.functions]
    Composition.hb_instance_168.f [var, in mathcomp.classical.functions]
    Composition.hb_instance_168.g [var, in mathcomp.classical.functions]
    Composition.hb_instance_171.f [var, in mathcomp.classical.functions]
    Composition.hb_instance_171.g [var, in mathcomp.classical.functions]
    Composition.hb_instance_177.f [var, in mathcomp.classical.functions]
    Composition.hb_instance_177.g [var, in mathcomp.classical.functions]
    Composition.hb_instance_183.f [var, in mathcomp.classical.functions]
    Composition.hb_instance_183.g [var, in mathcomp.classical.functions]
    Composition.hb_instance_189.f [var, in mathcomp.classical.functions]
    Composition.hb_instance_189.g [var, in mathcomp.classical.functions]
    Composition.hb_instance_192.f [var, in mathcomp.classical.functions]
    Composition.hb_instance_192.g [var, in mathcomp.classical.functions]
    Composition.hb_instance_198.f [var, in mathcomp.classical.functions]
    Composition.hb_instance_198.g [var, in mathcomp.classical.functions]
    Composition.hb_instance_204.f [var, in mathcomp.classical.functions]
    Composition.hb_instance_204.g [var, in mathcomp.classical.functions]
    Composition.hb_instance_210.f [var, in mathcomp.classical.functions]
    Composition.hb_instance_210.g [var, in mathcomp.classical.functions]
    Composition.hb_instance_216.f [var, in mathcomp.classical.functions]
    Composition.hb_instance_216.g [var, in mathcomp.classical.functions]
    Composition.OInv.f [var, in mathcomp.classical.functions]
    Composition.OInv.f [var, in mathcomp.classical.functions]
    Composition.OInv.g [var, in mathcomp.classical.functions]
    Composition.OInv.g [var, in mathcomp.classical.functions]
    Composition.rT [var, in mathcomp.classical.functions]
    Composition.rT [var, in mathcomp.classical.functions]
    Composition.sT [var, in mathcomp.classical.functions]
    Composition.sT [var, in mathcomp.classical.functions]
    compre_scale [prf, in mathcomp.analysis.ereal]
    compreBr [prf, in mathcomp.analysis.ereal]
    compreDr [prf, in mathcomp.analysis.ereal]
    compreN [prf, in mathcomp.analysis.ereal]
    comring.aT [var, in mathcomp.analysis.numfun]
    comring.hb_instance_23.f [var, in mathcomp.analysis.numfun]
    comring.hb_instance_23.g [var, in mathcomp.analysis.numfun]
    comring.rT [var, in mathcomp.analysis.numfun]
    concave_ln [prf, in mathcomp.analysis.exp]
    congr_lim [prf, in mathcomp.analysis.sequences]
    conjugate_powR [prf, in mathcomp.analysis.exp]
    connected [file, in mathcomp.analysis.topology_theory.connected]
    connected [def, in mathcomp.analysis.topology_theory.connected]
    connected0 [prf, in mathcomp.analysis.topology_theory.connected]
    connected1 [prf, in mathcomp.analysis.topology_theory.connected]
    connected_closure [prf, in mathcomp.analysis.topology_theory.connected]
    connected_component [def, in mathcomp.analysis.topology_theory.connected]
    connected_component_cover [prf, in mathcomp.analysis.topology_theory.connected]
    connected_component_id [prf, in mathcomp.analysis.topology_theory.connected]
    connected_component_max [prf, in mathcomp.analysis.topology_theory.connected]
    connected_component_out [prf, in mathcomp.analysis.topology_theory.connected]
    connected_component_refl [prf, in mathcomp.analysis.topology_theory.connected]
    connected_component_sub [prf, in mathcomp.analysis.topology_theory.connected]
    connected_component_sym [prf, in mathcomp.analysis.topology_theory.connected]
    connected_component_trans [prf, in mathcomp.analysis.topology_theory.connected]
    connected_continuous_connected [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    connected_intervalP [prf, in mathcomp.analysis.normedtype]
    connected_sets.T [var, in mathcomp.analysis.topology_theory.connected]
    connected_subset [prf, in mathcomp.analysis.topology_theory.connected]
    connectedP [prf, in mathcomp.analysis.topology_theory.connected]
    connectedPn [prf, in mathcomp.analysis.topology_theory.connected]
    connectedU [prf, in mathcomp.analysis.topology_theory.connected]
    constructive_ereal [file, in mathcomp.reals.constructive_ereal]
    constructive_ereal_dual_extended__canonical__choice_Choice [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_dual_extended__canonical__eqtype_Equality [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_dual_extended__canonical__GRing_Nmodule [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_EFin__canonical__GRing_Additive [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__choice_Choice [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__choice_Countable [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__classical_sets_Pointed [def, in mathcomp.analysis.ereal]
    constructive_ereal_extended__canonical__eqtype_Equality [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__filter_Filtered [def, in mathcomp.analysis.ereal]
    constructive_ereal_extended__canonical__filter_Nbhs [def, in mathcomp.analysis.ereal]
    constructive_ereal_extended__canonical__filter_PointedFiltered [def, in mathcomp.analysis.ereal]
    constructive_ereal_extended__canonical__filter_PointedNbhs [def, in mathcomp.analysis.ereal]
    constructive_ereal_extended__canonical__GRing_Nmodule [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__measure_AlgebraOfSets [def, in mathcomp.analysis.lebesgue_measure]
    constructive_ereal_extended__canonical__measure_Measurable [def, in mathcomp.analysis.lebesgue_measure]
    constructive_ereal_extended__canonical__measure_RingOfSets [def, in mathcomp.analysis.lebesgue_measure]
    constructive_ereal_extended__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.lebesgue_measure]
    constructive_ereal_extended__canonical__measure_SigmaRing [def, in mathcomp.analysis.lebesgue_measure]
    constructive_ereal_extended__canonical__Order_BDistrLattice [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__Order_BLattice [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__Order_BPOrder [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__Order_DistrLattice [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__Order_Lattice [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__Order_POrder [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__Order_TBDistrLattice [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__Order_TBLattice [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__Order_TBPOrder [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__Order_TLattice [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__Order_Total [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__Order_TPOrder [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_extended__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.ereal]
    constructive_ereal_extended__canonical__pseudometric_structure_PseudoPointedMetric [def, in mathcomp.analysis.ereal]
    constructive_ereal_extended__canonical__topology_structure_PointedTopological [def, in mathcomp.analysis.ereal]
    constructive_ereal_extended__canonical__topology_structure_Topological [def, in mathcomp.analysis.ereal]
    constructive_ereal_extended__canonical__uniform_structure_PointedUniform [def, in mathcomp.analysis.ereal]
    constructive_ereal_extended__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.ereal]
    constructive_ereal_mule__canonical__Monoid_ComLaw [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_mule__canonical__Monoid_Law [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_mule__canonical__Monoid_MulLaw [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_mule__canonical__SemiGroup_ComLaw [def, in mathcomp.reals.constructive_ereal]
    constructive_ereal_mule__canonical__SemiGroup_Law [def, in mathcomp.reals.constructive_ereal]
    constructive_indefinite_description [ax, in mathcomp.classical.boolp]
    ConstructiveDualAddTheory [mod, in mathcomp.reals.constructive_ereal]
    content [abbrev, in mathcomp.analysis.measure]
    Content [mod, in mathcomp.analysis.measure]
    Content.axioms_ [rec, in mathcomp.analysis.measure]
    Content.class [proj, in mathcomp.analysis.measure]
    Content.Exports [mod, in mathcomp.analysis.measure]
    Content.measure_isContent_mixin [proj, in mathcomp.analysis.measure]
    Content.pack_ [def, in mathcomp.analysis.measure]
    Content.phant_clone [def, in mathcomp.analysis.measure]
    Content.phant_on_ [def, in mathcomp.analysis.measure]
    Content.sort [proj, in mathcomp.analysis.measure]
    Content.type [rec, in mathcomp.analysis.measure]
    content_fin_bigcup [prf, in mathcomp.analysis.measure]
    Content_isMeasure [mod, in mathcomp.analysis.measure]
    Content_isMeasure.axioms_ [rec, in mathcomp.analysis.measure]
    Content_isMeasure.Content_isMeasure.d [var, in mathcomp.analysis.measure]
    Content_isMeasure.Content_isMeasure.local_mixin_measure_isContent [var, in mathcomp.analysis.measure]
    Content_isMeasure.Content_isMeasure.mu [var, in mathcomp.analysis.measure]
    Content_isMeasure.Content_isMeasure.R [var, in mathcomp.analysis.measure]
    Content_isMeasure.Content_isMeasure.T [var, in mathcomp.analysis.measure]
    Content_isMeasure.Content_isMeasure_mu__canonical__measure_Content [def, in mathcomp.analysis.measure]
    Content_isMeasure.Exports [mod, in mathcomp.analysis.measure]
    Content_isMeasure.identity_builder [def, in mathcomp.analysis.measure]
    Content_isMeasure.measure_semi_sigma_additive [proj, in mathcomp.analysis.measure]
    Content_isMeasure.phant_axioms [def, in mathcomp.analysis.measure]
    Content_isMeasure.phant_Build [def, in mathcomp.analysis.measure]
    content_on_ring_of_sets.d [var, in mathcomp.analysis.measure]
    content_on_ring_of_sets.mu [var, in mathcomp.analysis.measure]
    content_on_ring_of_sets.R [var, in mathcomp.analysis.measure]
    content_on_ring_of_sets.T [var, in mathcomp.analysis.measure]
    content_on_semiring_of_sets.d [var, in mathcomp.analysis.measure]
    content_on_semiring_of_sets.mu [var, in mathcomp.analysis.measure]
    content_on_semiring_of_sets.R [var, in mathcomp.analysis.measure]
    content_on_semiring_of_sets.T [var, in mathcomp.analysis.measure]
    content_ring_lemmas.d [var, in mathcomp.analysis.measure]
    content_ring_lemmas.mu [var, in mathcomp.analysis.measure]
    content_ring_lemmas.R [var, in mathcomp.analysis.measure]
    content_ring_lemmas.T [var, in mathcomp.analysis.measure]
    content_ring_sigma_additive [prf, in mathcomp.analysis.measure]
    content_ring_sup_sigma_additive [prf, in mathcomp.analysis.measure]
    content_ringOfSetsType.d [var, in mathcomp.analysis.measure]
    content_ringOfSetsType.mu [var, in mathcomp.analysis.measure]
    content_ringOfSetsType.R [var, in mathcomp.analysis.measure]
    content_ringOfSetsType.T [var, in mathcomp.analysis.measure]
    content_semiRingOfSetsType.A [var, in mathcomp.analysis.measure]
    content_semiRingOfSetsType.B [var, in mathcomp.analysis.measure]
    content_semiRingOfSetsType.d [var, in mathcomp.analysis.measure]
    content_semiRingOfSetsType.mA [var, in mathcomp.analysis.measure]
    content_semiRingOfSetsType.mB [var, in mathcomp.analysis.measure]
    content_semiRingOfSetsType.mu [var, in mathcomp.analysis.measure]
    content_semiRingOfSetsType.R [var, in mathcomp.analysis.measure]
    content_semiRingOfSetsType.T [var, in mathcomp.analysis.measure]
    Content_SigmaSubAdditive_isMeasure [mod, in mathcomp.analysis.measure]
    Content_SigmaSubAdditive_isMeasure.axioms_ [rec, in mathcomp.analysis.measure]
    Content_SigmaSubAdditive_isMeasure.Content_SigmaSubAdditive_isMeasure.d [var, in mathcomp.analysis.measure]
    Content_SigmaSubAdditive_isMeasure.Content_SigmaSubAdditive_isMeasure.local_mixin_measure_isContent [var, in mathcomp.analysis.measure]
    Content_SigmaSubAdditive_isMeasure.Content_SigmaSubAdditive_isMeasure.mu [var, in mathcomp.analysis.measure]
    Content_SigmaSubAdditive_isMeasure.Content_SigmaSubAdditive_isMeasure.R [var, in mathcomp.analysis.measure]
    Content_SigmaSubAdditive_isMeasure.Content_SigmaSubAdditive_isMeasure.T [var, in mathcomp.analysis.measure]
    Content_SigmaSubAdditive_isMeasure.Content_SigmaSubAdditive_isMeasure_mu__canonical__measure_Content [def, in mathcomp.analysis.measure]
    Content_SigmaSubAdditive_isMeasure.Exports [mod, in mathcomp.analysis.measure]
    Content_SigmaSubAdditive_isMeasure.measure_sigma_subadditive [proj, in mathcomp.analysis.measure]
    Content_SigmaSubAdditive_isMeasure.phant_axioms [def, in mathcomp.analysis.measure]
    Content_SigmaSubAdditive_isMeasure.phant_Build [def, in mathcomp.analysis.measure]
    content_signed.d [var, in mathcomp.analysis.measure]
    content_signed.mu [var, in mathcomp.analysis.measure]
    content_signed.R [var, in mathcomp.analysis.measure]
    content_signed.T [var, in mathcomp.analysis.measure]
    content_snum [def, in mathcomp.analysis.measure]
    content_snum_subproof [prf, in mathcomp.analysis.measure]
    content_sub_additive [abbrev, in mathcomp.analysis.measure]
    content_sub_fsum [prf, in mathcomp.analysis.measure]
    content_subadditive [prf, in mathcomp.analysis.measure]
    ContentElpiOperations [mod, in mathcomp.analysis.measure]
    continuity_eq [prf, in mathcomp.reals_stdlib.Rstruct]
    continuity_exp [prf, in mathcomp.reals_stdlib.Rstruct]
    continuity_pt_cvg [prf, in mathcomp.analysis_stdlib.Rstruct_topology]
    continuity_pt_cvg' [prf, in mathcomp.analysis_stdlib.Rstruct_topology]
    continuity_pt_dnbhs [prf, in mathcomp.analysis_stdlib.Rstruct_topology]
    continuity_pt_nbhs [prf, in mathcomp.analysis_stdlib.Rstruct_topology]
    continuity_ptE [prf, in mathcomp.analysis_stdlib.Rstruct_topology]
    continuity_sum [prf, in mathcomp.reals_stdlib.Rstruct]
    continuous [abbrev, in mathcomp.classical.filter]
    Continuous [mod, in mathcomp.analysis.topology_theory.topology_structure]
    Continuous.axioms_ [rec, in mathcomp.analysis.topology_theory.topology_structure]
    Continuous.class [proj, in mathcomp.analysis.topology_theory.topology_structure]
    Continuous.Exports [mod, in mathcomp.analysis.topology_theory.topology_structure]
    continuous.K [var, in mathcomp.analysis.normedtype]
    Continuous.pack_ [def, in mathcomp.analysis.topology_theory.topology_structure]
    Continuous.phant_clone [def, in mathcomp.analysis.topology_theory.topology_structure]
    Continuous.phant_on_ [def, in mathcomp.analysis.topology_theory.topology_structure]
    Continuous.sort [proj, in mathcomp.analysis.topology_theory.topology_structure]
    Continuous.topology_structure_isContinuous_mixin [proj, in mathcomp.analysis.topology_theory.topology_structure]
    Continuous.type [rec, in mathcomp.analysis.topology_theory.topology_structure]
    continuous.U [var, in mathcomp.analysis.normedtype]
    continuous.V [var, in mathcomp.analysis.normedtype]
    continuous2_cvg [prf, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_acos [prf, in mathcomp.analysis.trigo]
    continuous_asin [prf, in mathcomp.analysis.trigo]
    continuous_at [def, in mathcomp.classical.filter]
    continuous_atan [prf, in mathcomp.analysis.trigo]
    continuous_bounded_extension [prf, in mathcomp.analysis.numfun]
    continuous_closedP [prf, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_comp [prf, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_comp.f [var, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_comp.g [var, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_comp.X [var, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_comp.Y [var, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_comp.Z [var, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_comp_subproof [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_comp_weak [prf, in mathcomp.analysis.topology_theory.weak_topology]
    continuous_compact [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_compact_integrable [prf, in mathcomp.analysis.lebesgue_integral]
    continuous_const.X [var, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_const.y [var, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_const.Y [var, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_cos [prf, in mathcomp.analysis.trigo]
    continuous_curry [prf, in mathcomp.analysis.function_spaces]
    continuous_curry_cvg [prf, in mathcomp.analysis.function_spaces]
    continuous_curry_fun [prf, in mathcomp.analysis.function_spaces]
    continuous_cvg [prf, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_cvg_davg [prf, in mathcomp.analysis.lebesgue_integral]
    continuous_cvg_dist [abbrev, in mathcomp.analysis.normedtype]
    continuous_density_L1.mu [var, in mathcomp.analysis.lebesgue_integral]
    continuous_density_L1.R [var, in mathcomp.analysis.lebesgue_integral]
    continuous_density_L1.rT [var, in mathcomp.analysis.lebesgue_integral]
    continuous_expR [prf, in mathcomp.analysis.exp]
    continuous_FTC1 [prf, in mathcomp.analysis.ftc]
    continuous_FTC1_closed [prf, in mathcomp.analysis.ftc]
    continuous_FTC2 [prf, in mathcomp.analysis.ftc]
    continuous_fun_comp.A [var, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_fun_comp.B [var, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_fun_comp.C [var, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_fun_comp.f [var, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_fun_comp.g [var, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_fun_comp.X [var, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_fun_comp.Y [var, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_fun_comp.Z [var, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_id.X [var, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_in_subspaceT [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_inj_image_segment [prf, in mathcomp.analysis.realfun]
    continuous_inj_image_segmentP [prf, in mathcomp.analysis.realfun]
    continuous_inP [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_is_cvg [prf, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_lebesgue_pt [prf, in mathcomp.analysis.lebesgue_integral]
    continuous_lim_sup_davg [prf, in mathcomp.analysis.lebesgue_integral]
    continuous_linear_bounded [prf, in mathcomp.analysis.normedtype]
    continuous_ln [prf, in mathcomp.analysis.exp]
    continuous_localP [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_max [prf, in mathcomp.analysis.normedtype]
    continuous_measurable_fun [prf, in mathcomp.analysis.lebesgue_measure]
    continuous_min [prf, in mathcomp.analysis.normedtype]
    continuous_open_subspace [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_path [file, in mathcomp.analysis.homotopy_theory.continuous_path]
    continuous_path_chain_path__canonical__continuous_path_Path [def, in mathcomp.analysis.homotopy_theory.continuous_path]
    continuous_path_chain_path__canonical__topology_structure_Continuous [def, in mathcomp.analysis.homotopy_theory.continuous_path]
    continuous_path_mk_path__canonical__continuous_path_Path [def, in mathcomp.analysis.homotopy_theory.continuous_path]
    continuous_path_mk_path__canonical__topology_structure_Continuous [def, in mathcomp.analysis.homotopy_theory.continuous_path]
    continuous_path_reparameterize__canonical__continuous_path_Path [def, in mathcomp.analysis.homotopy_theory.continuous_path]
    continuous_path_reparameterize__canonical__topology_structure_Continuous [def, in mathcomp.analysis.homotopy_theory.continuous_path]
    continuous_shift [prf, in mathcomp.analysis.normedtype]
    continuous_sin [prf, in mathcomp.analysis.trigo]
    continuous_subspace0 [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_subspace1 [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_subspace_in [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_subspace_itv [prf, in mathcomp.analysis.realfun]
    continuous_subspace_prodP [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_subspace_setT [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_subspaceT [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_subspaceT_for [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_subspaceW [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    continuous_tan [prf, in mathcomp.analysis.trigo]
    Continuous_type__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.topology_structure]
    Continuous_type__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.topology_structure]
    continuous_uncurry [prf, in mathcomp.analysis.function_spaces]
    continuous_uncurry_regular [prf, in mathcomp.analysis.function_spaces]
    continuous_within_itvcyP [prf, in mathcomp.analysis.normedtype]
    continuous_within_itvNycP [prf, in mathcomp.analysis.normedtype]
    continuous_within_itvP [prf, in mathcomp.analysis.normedtype]
    continuous_within_itvP.near_at_left [var, in mathcomp.analysis.normedtype]
    continuous_within_itvP.near_at_right [var, in mathcomp.analysis.normedtype]
    continuous_within_itvP.R [var, in mathcomp.analysis.normedtype]
    continuous_withinNshiftx [prf, in mathcomp.analysis.normedtype]
    continuous_withinNx [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    continuousB [prf, in mathcomp.analysis.normedtype]
    continuousD [prf, in mathcomp.analysis.normedtype]
    ContinuousElpiOperations [mod, in mathcomp.analysis.topology_theory.topology_structure]
    continuousEP [prf, in mathcomp.analysis.topology_theory.topology_structure]
    continuousfor0_continuous [prf, in mathcomp.analysis.normedtype]
    ContinuousFun [mod, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.axioms_ [rec, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.class [proj, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.Exports [mod, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.Exports.join_subspace_topology_ContinuousFun_between_topology_structure_Continuous_and_functions_Fun [def, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.Exports.subspace_topology_ContinuousFun__to__functions_Fun [def, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.Exports.subspace_topology_ContinuousFun__to__topology_structure_Continuous [def, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.Exports.subspace_topology_ContinuousFun_class__to__functions_Fun_class [def, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.Exports.subspace_topology_ContinuousFun_class__to__topology_structure_Continuous_class [def, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.functions_isFun_mixin [proj, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.pack_ [def, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.phant_clone [def, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.phant_on_ [def, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.sort [proj, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.topology_structure_isContinuous_mixin [proj, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFun.type [rec, in mathcomp.analysis.topology_theory.subspace_topology]
    ContinuousFunElpiOperations [mod, in mathcomp.analysis.topology_theory.subspace_topology]
    continuousM [prf, in mathcomp.analysis.normedtype]
    continuousN [prf, in mathcomp.analysis.normedtype]
    continuousP [prf, in mathcomp.analysis.topology_theory.topology_structure]
    continuousV [prf, in mathcomp.analysis.normedtype]
    continuousZ [prf, in mathcomp.analysis.normedtype]
    continuousZl [prf, in mathcomp.analysis.normedtype]
    continuousZr [prf, in mathcomp.analysis.normedtype]
    contra [file, in mathcomp.classical.contra]
    contra_eqP [prf, in mathcomp.classical.boolp]
    contra_leP [prf, in mathcomp.classical.boolp]
    contra_ltP [prf, in mathcomp.classical.boolp]
    contra_neqP [prf, in mathcomp.classical.boolp]
    contra_notP [prf, in mathcomp.classical.boolp]
    contra_notT [prf, in mathcomp.classical.boolp]
    contract [def, in mathcomp.reals.constructive_ereal]
    contract0 [prf, in mathcomp.reals.constructive_ereal]
    contract_eq0 [prf, in mathcomp.analysis.ereal]
    contract_eq1 [prf, in mathcomp.analysis.ereal]
    contract_eqN1 [prf, in mathcomp.analysis.ereal]
    contract_ereal_ball_fin_le [prf, in mathcomp.analysis.ereal]
    contract_ereal_ball_fin_lt [prf, in mathcomp.analysis.ereal]
    contract_ereal_ball_pinfty [prf, in mathcomp.reals.constructive_ereal]
    contract_expand.R [var, in mathcomp.reals.constructive_ereal]
    contract_expand.R [var, in mathcomp.analysis.ereal]
    contract_expand_realType.contract [var, in mathcomp.analysis.ereal]
    contract_expand_realType.R [var, in mathcomp.analysis.ereal]
    contract_imageN [prf, in mathcomp.analysis.ereal]
    contract_inf [prf, in mathcomp.analysis.ereal]
    contract_inj [def, in mathcomp.reals.constructive_ereal]
    contract_le1 [prf, in mathcomp.reals.constructive_ereal]
    contract_lt1 [prf, in mathcomp.reals.constructive_ereal]
    contract_sup [prf, in mathcomp.analysis.ereal]
    contraction [def, in mathcomp.analysis.normedtype]
    contraction_cvg [prf, in mathcomp.analysis.sequences]
    contraction_cvg_fixed [prf, in mathcomp.analysis.sequences]
    contraction_dist [prf, in mathcomp.analysis.sequences]
    contraction_fixpoint_unique [prf, in mathcomp.analysis.normedtype]
    contractions.R [var, in mathcomp.analysis.normedtype]
    contractions.U [var, in mathcomp.analysis.normedtype]
    contractions.V [var, in mathcomp.analysis.normedtype]
    contractions.X [var, in mathcomp.analysis.normedtype]
    contractions.Y [var, in mathcomp.analysis.normedtype]
    contractK [prf, in mathcomp.analysis.ereal]
    contractN [prf, in mathcomp.reals.constructive_ereal]
    contraNP [prf, in mathcomp.classical.boolp]
    contraPP [prf, in mathcomp.classical.boolp]
    contraPT [prf, in mathcomp.classical.boolp]
    contrapT [prf, in mathcomp.classical.boolp]
    contraTP [prf, in mathcomp.classical.boolp]
    conv [def, in mathcomp.analysis.convex]
    conv0 [def, in mathcomp.analysis.convex]
    conv1 [prf, in mathcomp.analysis.convex]
    conv_gt0 [prf, in mathcomp.analysis.convex]
    conv_realDomainType.R [var, in mathcomp.analysis.convex]
    convA [def, in mathcomp.analysis.convex]
    convC [def, in mathcomp.analysis.convex]
    convex [file, in mathcomp.analysis.convex]
    convex [abbrev, in mathcomp.experimental_reals.distr]
    convex [abbrev, in mathcomp.experimental_reals.distr]
    convex [def, in mathcomp.analysis.tvs]
    convex_E__canonical__choice_Choice [def, in mathcomp.analysis.convex]
    convex_E__canonical__convex_ConvexSpace [def, in mathcomp.analysis.convex]
    convex_E__canonical__eqtype_Equality [def, in mathcomp.analysis.convex]
    convex_expR [prf, in mathcomp.analysis.exp]
    convex_function [def, in mathcomp.analysis.convex]
    convex_lmodType [def, in mathcomp.analysis.convex]
    convex_powR [prf, in mathcomp.analysis.hoelder]
    convex_powR.R [var, in mathcomp.analysis.hoelder]
    convex_realDomainType [def, in mathcomp.analysis.convex]
    convex_space_lemmas.A [var, in mathcomp.analysis.convex]
    convex_space_lemmas.R [var, in mathcomp.analysis.convex]
    convexon [def, in mathcomp.experimental_reals.distr]
    ConvexSpace [mod, in mathcomp.analysis.convex]
    ConvexSpace.axioms_ [rec, in mathcomp.analysis.convex]
    ConvexSpace.choice_hasChoice_mixin [proj, in mathcomp.analysis.convex]
    ConvexSpace.class [proj, in mathcomp.analysis.convex]
    ConvexSpace.convex_isConvexSpace_mixin [proj, in mathcomp.analysis.convex]
    ConvexSpace.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.convex]
    ConvexSpace.Exports [mod, in mathcomp.analysis.convex]
    ConvexSpace.Exports.convex_ConvexSpace__to__choice_Choice [def, in mathcomp.analysis.convex]
    ConvexSpace.Exports.convex_ConvexSpace__to__eqtype_Equality [def, in mathcomp.analysis.convex]
    ConvexSpace.Exports.convex_ConvexSpace_class__to__choice_Choice_class [def, in mathcomp.analysis.convex]
    ConvexSpace.Exports.convex_ConvexSpace_class__to__eqtype_Equality_class [def, in mathcomp.analysis.convex]
    ConvexSpace.pack_ [def, in mathcomp.analysis.convex]
    ConvexSpace.phant_clone [def, in mathcomp.analysis.convex]
    ConvexSpace.phant_on_ [def, in mathcomp.analysis.convex]
    ConvexSpace.sort [proj, in mathcomp.analysis.convex]
    ConvexSpace.type [rec, in mathcomp.analysis.convex]
    ConvexSpaceElpiOperations [mod, in mathcomp.analysis.convex]
    convmm [def, in mathcomp.analysis.convex]
    convRE [prf, in mathcomp.analysis.convex]
    coord_continuous [prf, in mathcomp.analysis.normedtype]
    corollary_FTC1.R [var, in mathcomp.analysis.ftc]
    corollary_FTC1.within_continuous_restrict [var, in mathcomp.analysis.ftc]
    cos [mod, in mathcomp.analysis.trigo]
    cos.body [def, in mathcomp.analysis.trigo]
    cos.unlock [def, in mathcomp.analysis.trigo]
    cos0 [prf, in mathcomp.analysis.trigo]
    cos1_gt0 [prf, in mathcomp.analysis.trigo]
    cos1sin0 [prf, in mathcomp.analysis.trigo]
    cos2_lt0 [prf, in mathcomp.analysis.trigo]
    cos2_tan2 [prf, in mathcomp.analysis.trigo]
    cos2Dsin2 [prf, in mathcomp.analysis.trigo]
    cos2pi [prf, in mathcomp.analysis.trigo]
    cos2sin2 [prf, in mathcomp.analysis.trigo]
    cos_02_uniq [prf, in mathcomp.analysis.trigo]
    cos_asin [prf, in mathcomp.analysis.trigo]
    cos_atan [prf, in mathcomp.analysis.trigo]
    cos_coeff [def, in mathcomp.analysis.trigo]
    cos_coeff' [def, in mathcomp.analysis.trigo]
    cos_coeff'E [prf, in mathcomp.analysis.trigo]
    cos_coeff_2_0 [prf, in mathcomp.analysis.trigo]
    cos_coeff_2_2 [prf, in mathcomp.analysis.trigo]
    cos_coeff_2_4 [prf, in mathcomp.analysis.trigo]
    cos_coeff_odd [prf, in mathcomp.analysis.trigo]
    cos_coeffE [prf, in mathcomp.analysis.trigo]
    cos_exists [prf, in mathcomp.analysis.trigo]
    cos_ge0_pihalf [prf, in mathcomp.analysis.trigo]
    cos_geN1 [prf, in mathcomp.analysis.trigo]
    cos_gt0_pihalf [prf, in mathcomp.analysis.trigo]
    cos_inj [prf, in mathcomp.analysis.trigo]
    cos_le1 [prf, in mathcomp.analysis.trigo]
    cos_Locked [modtype, in mathcomp.analysis.trigo]
    cos_Locked.body [ax, in mathcomp.analysis.trigo]
    cos_Locked.unlock [ax, in mathcomp.analysis.trigo]
    cos_max [prf, in mathcomp.analysis.trigo]
    cos_mulr2n [prf, in mathcomp.analysis.trigo]
    cos_norm [prf, in mathcomp.analysis.trigo]
    cos_pihalf [prf, in mathcomp.analysis.trigo]
    cos_sg [prf, in mathcomp.analysis.trigo]
    cos_unlock_subterm [def, in mathcomp.analysis.trigo]
    cosB [prf, in mathcomp.analysis.trigo]
    cosBpihalf [prf, in mathcomp.analysis.trigo]
    cosD [prf, in mathcomp.reals_stdlib.Rstruct]
    cosD [prf, in mathcomp.analysis.trigo]
    cosD2pi [prf, in mathcomp.analysis.trigo]
    cosDpi [prf, in mathcomp.analysis.trigo]
    cosDpihalf [prf, in mathcomp.analysis.trigo]
    cosE [prf, in mathcomp.analysis.trigo]
    cosK [prf, in mathcomp.analysis.trigo]
    cosKN [prf, in mathcomp.analysis.trigo]
    cosN [prf, in mathcomp.analysis.trigo]
    cospi [prf, in mathcomp.analysis.trigo]
    CosSin.R [var, in mathcomp.analysis.trigo]
    Countable [constr, in mathcomp.experimental_reals.discrete]
    countable [ind, in mathcomp.experimental_reals.discrete]
    countable [def, in mathcomp.classical.cardinality]
    Countable.E [var, in mathcomp.experimental_reals.discrete]
    Countable.T [var, in mathcomp.experimental_reals.discrete]
    countable0 [prf, in mathcomp.classical.cardinality]
    countable1 [prf, in mathcomp.classical.cardinality]
    countable_bigcupT_measurable [prf, in mathcomp.analysis.measure]
    countable_bijP [prf, in mathcomp.classical.cardinality]
    countable_choiceMixin [def, in mathcomp.experimental_reals.discrete]
    countable_countable [prf, in mathcomp.experimental_reals.discrete]
    countable_countMixin [def, in mathcomp.experimental_reals.discrete]
    countable_finite_subset [prf, in mathcomp.classical.cardinality]
    countable_finpred [prf, in mathcomp.classical.cardinality]
    countable_fset [prf, in mathcomp.classical.cardinality]
    countable_injP [prf, in mathcomp.classical.cardinality]
    countable_measurable [prf, in mathcomp.analysis.measure]
    countable_n_subset [prf, in mathcomp.classical.cardinality]
    countable_range [def, in mathcomp.analysis.probability]
    countable_set0 [abbrev, in mathcomp.classical.cardinality]
    countable_sub [prf, in mathcomp.experimental_reals.discrete]
    countable_sup_ent [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    countable_uniform [abbrev, in mathcomp.analysis.separation_axioms]
    countable_uniform [mod, in mathcomp.analysis.separation_axioms]
    countable_uniform.classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform.cnt_unif [var, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform.entF [var, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform.entG [var, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform.f_ [var, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform.hb_instance_16.q [var, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform.R [var, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform.T [var, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_bounded [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_type__canonical__choice_Choice [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_type__canonical__classical_sets_Pointed [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_type__canonical__eqtype_Equality [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_type__canonical__filter_Filtered [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_type__canonical__filter_Nbhs [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_type__canonical__filter_PointedFiltered [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_type__canonical__filter_PointedNbhs [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_type__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_type__canonical__pseudometric_structure_PseudoPointedMetric [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_type__canonical__topology_structure_PointedTopological [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_type__canonical__topology_structure_Topological [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_type__canonical__uniform_structure_PointedUniform [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countable_uniform_type__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.countableBase [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.countableBaseG [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.descendG [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.descendG1 [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.distN [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.distN0 [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.distN_half [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.distN_le [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.distN_nat [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.entourage_nball [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.Exports [mod, in mathcomp.analysis.separation_axioms]
    countable_uniform.g_ [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.gsubf [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.HB_unnamed_factory_1 [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.HB_unnamed_factory_14 [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.HB_unnamed_factory_17 [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.HB_unnamed_mixin_10 [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.HB_unnamed_mixin_11 [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.HB_unnamed_mixin_12 [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.HB_unnamed_mixin_13 [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.HB_unnamed_mixin_21 [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.HB_unnamed_mixin_8 [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.HB_unnamed_mixin_9 [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.n_step_ball [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.n_step_ball_center [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.n_step_ball_le [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.n_step_ball_le_g [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.n_step_ball_pos [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.n_step_ball_sym [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.n_step_ball_triangle [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.split_n_step_ball [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.splitG3 [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.step_ball [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.step_ball_center [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.step_ball_entourage [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.step_ball_le [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.step_ball_pos [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.step_ball_sym [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.step_ball_triangle [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.subset_n_step_ball [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.subset_step_ball [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.symG [prf, in mathcomp.analysis.separation_axioms]
    countable_uniform.type [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.uniform_structure_Uniform__to__choice_hasChoice [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.uniform_structure_Uniform__to__eqtype_hasDecEq [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.uniform_structure_Uniform__to__filter_isFiltered [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.uniform_structure_Uniform__to__filter_selfFiltered [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.uniform_structure_Uniform__to__topology_structure_Nbhs_isTopological [def, in mathcomp.analysis.separation_axioms]
    countable_uniform.uniform_structure_Uniform__to__uniform_structure_Nbhs_isUniform_mixin [def, in mathcomp.analysis.separation_axioms]
    countable_uniformity [def, in mathcomp.analysis.topology_theory.uniform_structure]
    countable_uniformity_metric [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    countable_uniformityP [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    countableM [abbrev, in mathcomp.classical.cardinality]
    countableML [abbrev, in mathcomp.classical.cardinality]
    countableMR [abbrev, in mathcomp.classical.cardinality]
    countableP [prf, in mathcomp.classical.cardinality]
    CountableTheory.CanCountable.E [var, in mathcomp.experimental_reals.discrete]
    CountableTheory.CanCountable.f [var, in mathcomp.experimental_reals.discrete]
    CountableTheory.CanCountable.g [var, in mathcomp.experimental_reals.discrete]
    CountableTheory.CanCountable.T [var, in mathcomp.experimental_reals.discrete]
    CountableTheory.CanCountable.U [var, in mathcomp.experimental_reals.discrete]
    CountableTheory.CountType.c [var, in mathcomp.experimental_reals.discrete]
    CountableTheory.CountType.E [var, in mathcomp.experimental_reals.discrete]
    CountableTheory.CountType.T [var, in mathcomp.experimental_reals.discrete]
    CountableUnion.cE [var, in mathcomp.experimental_reals.discrete]
    CountableUnion.E [var, in mathcomp.experimental_reals.discrete]
    CountableUnion.T [var, in mathcomp.experimental_reals.discrete]
    countableX [prf, in mathcomp.classical.cardinality]
    countableXL [prf, in mathcomp.classical.cardinality]
    countableXR [prf, in mathcomp.classical.cardinality]
    counting [abbrev, in mathcomp.analysis.measure]
    counting [def, in mathcomp.analysis.measure]
    counting_dirac [prf, in mathcomp.analysis.lebesgue_integral]
    CountSub.E [var, in mathcomp.experimental_reals.discrete]
    CountSub.F [var, in mathcomp.experimental_reals.discrete]
    CountSub.T [var, in mathcomp.experimental_reals.discrete]
    coutinuous_measurable.R [var, in mathcomp.analysis.lebesgue_measure]
    covariance [mod, in mathcomp.analysis.probability]
    covariance.body [def, in mathcomp.analysis.probability]
    covariance.unlock [def, in mathcomp.analysis.probability]
    covariance_cst_l [prf, in mathcomp.analysis.probability]
    covariance_cst_r [prf, in mathcomp.analysis.probability]
    covariance_fin_num [prf, in mathcomp.analysis.probability]
    covariance_le [prf, in mathcomp.analysis.probability]
    covariance_lemmas.d [var, in mathcomp.analysis.probability]
    covariance_lemmas.P [var, in mathcomp.analysis.probability]
    covariance_lemmas.R [var, in mathcomp.analysis.probability]
    covariance_lemmas.T [var, in mathcomp.analysis.probability]
    covariance_Locked [modtype, in mathcomp.analysis.probability]
    covariance_Locked.body [ax, in mathcomp.analysis.probability]
    covariance_Locked.unlock [ax, in mathcomp.analysis.probability]
    covariance_unlock_subterm [def, in mathcomp.analysis.probability]
    covariance_unlockable [def, in mathcomp.analysis.probability]
    covarianceBl [prf, in mathcomp.analysis.probability]
    covarianceBr [prf, in mathcomp.analysis.probability]
    covarianceC [prf, in mathcomp.analysis.probability]
    covarianceDl [prf, in mathcomp.analysis.probability]
    covarianceDr [prf, in mathcomp.analysis.probability]
    covarianceE [prf, in mathcomp.analysis.probability]
    covarianceNl [prf, in mathcomp.analysis.probability]
    covarianceNN [prf, in mathcomp.analysis.probability]
    covarianceNr [prf, in mathcomp.analysis.probability]
    covarianceZl [prf, in mathcomp.analysis.probability]
    covarianceZr [prf, in mathcomp.analysis.probability]
    cover [def, in mathcomp.classical.classical_sets]
    cover_compact [def, in mathcomp.analysis.topology_theory.compact]
    cover_compactE [prf, in mathcomp.analysis.topology_theory.compact]
    cover_measurable [prf, in mathcomp.analysis.measure]
    cover_restr [prf, in mathcomp.classical.classical_sets]
    cover_subset [prf, in mathcomp.analysis.measure]
    cover_vitali_collection_partition [prf, in mathcomp.analysis.normedtype]
    coverE [prf, in mathcomp.classical.classical_sets]
    covered_by [def, in mathcomp.analysis.measure]
    covered_by_countable [prf, in mathcomp.analysis.measure]
    covered_by_finite [prf, in mathcomp.analysis.measure]
    covered_byP [prf, in mathcomp.analysis.measure]
    covered_bySr [prf, in mathcomp.analysis.measure]
    covering.T [var, in mathcomp.analysis.measure]
    Covers.T [var, in mathcomp.analysis.topology_theory.compact]
    cp01_clamp [def, in mathcomp.experimental_reals.distr]
    cpoint [def, in mathcomp.analysis.normedtype]
    cpoint_ball [prf, in mathcomp.analysis.normedtype]
    cpoint_scale_ball [prf, in mathcomp.analysis.normedtype]
    crestr [def, in mathcomp.analysis.charge]
    crestr0 [def, in mathcomp.analysis.charge]
    cscale [def, in mathcomp.analysis.charge]
    cst [def, in mathcomp.classical.functions]
    cst_continuous [prf, in mathcomp.analysis.topology_theory.topology_structure]
    cst_fimfun [def, in mathcomp.classical.cardinality]
    cst_nnfun_subproof [prf, in mathcomp.analysis.lebesgue_integral]
    cst_nnsfun [def, in mathcomp.analysis.lebesgue_integral]
    cst_path.i [var, in mathcomp.analysis.homotopy_theory.continuous_path]
    cst_path.T [var, in mathcomp.analysis.homotopy_theory.continuous_path]
    cst_path.x [var, in mathcomp.analysis.homotopy_theory.continuous_path]
    cst_sfun [def, in mathcomp.analysis.lebesgue_integral]
    cst_sfunE [prf, in mathcomp.analysis.lebesgue_integral]
    cstE [prf, in mathcomp.classical.functions]
    cts_const [prf, in mathcomp.analysis.topology_theory.topology_structure]
    cts_fun [def, in mathcomp.analysis.topology_theory.topology_structure]
    cts_fun_comp [prf, in mathcomp.analysis.topology_theory.topology_structure]
    cts_id [prf, in mathcomp.analysis.topology_theory.topology_structure]
    Cumulative [mod, in mathcomp.analysis.lebesgue_stieltjes_measure]
    Cumulative.axioms_ [rec, in mathcomp.analysis.lebesgue_stieltjes_measure]
    Cumulative.class [proj, in mathcomp.analysis.lebesgue_stieltjes_measure]
    Cumulative.Exports [mod, in mathcomp.analysis.lebesgue_stieltjes_measure]
    Cumulative.lebesgue_stieltjes_measure_isCumulative_mixin [proj, in mathcomp.analysis.lebesgue_stieltjes_measure]
    Cumulative.pack_ [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
    Cumulative.phant_clone [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
    Cumulative.phant_on_ [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
    Cumulative.sort [proj, in mathcomp.analysis.lebesgue_stieltjes_measure]
    Cumulative.type [rec, in mathcomp.analysis.lebesgue_stieltjes_measure]
    cumulative_content_sub_fsum [prf, in mathcomp.analysis.lebesgue_stieltjes_measure]
    cumulative_is_nondecreasing [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
    cumulative_is_right_continuous [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
    CumulativeElpiOperations [mod, in mathcomp.analysis.lebesgue_stieltjes_measure]
    cunion_countable [prf, in mathcomp.experimental_reals.discrete]
    curry_continuous [prf, in mathcomp.analysis.function_spaces]
    currying.cartesian_closed.U [var, in mathcomp.analysis.function_spaces]
    currying.cartesian_closed.V [var, in mathcomp.analysis.function_spaces]
    currying.cartesian_closed.W [var, in mathcomp.analysis.function_spaces]
    curryK [prf, in mathcomp.classical.boolp]
    cvg [abbrev, in mathcomp.classical.filter]
    cvg_0_pinfty.a [var, in mathcomp.analysis.normedtype]
    cvg_0_pinfty.FF [var, in mathcomp.analysis.normedtype]
    cvg_0_pinfty.I [var, in mathcomp.analysis.normedtype]
    cvg_0_pinfty.R [var, in mathcomp.analysis.normedtype]
    cvg_abse [prf, in mathcomp.analysis.normedtype]
    cvg_abse0P [prf, in mathcomp.analysis.normedtype]
    cvg_addnl [prf, in mathcomp.analysis.topology_theory.nat_topology]
    cvg_addnr [prf, in mathcomp.analysis.topology_theory.nat_topology]
    cvg_addrl [prf, in mathcomp.analysis.realfun]
    cvg_addrr [prf, in mathcomp.analysis.realfun]
    cvg_app [prf, in mathcomp.classical.filter]
    cvg_app_entourageP [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    cvg_app_within [prf, in mathcomp.analysis.topology_theory.topology_structure]
    cvg_approx [prf, in mathcomp.analysis.lebesgue_integral]
    cvg_arithmetic [prf, in mathcomp.analysis.sequences]
    cvg_at_left_filter [prf, in mathcomp.analysis.normedtype]
    cvg_at_left_within [prf, in mathcomp.analysis.normedtype]
    cvg_at_leftE [prf, in mathcomp.analysis.normedtype]
    cvg_at_leftE [prf, in mathcomp.analysis.derive]
    cvg_at_leftNP [prf, in mathcomp.analysis.normedtype]
    cvg_at_leftP [prf, in mathcomp.analysis.realfun]
    cvg_at_right_filter [prf, in mathcomp.analysis.normedtype]
    cvg_at_right_left_dnbhs [prf, in mathcomp.analysis.realfun]
    cvg_at_right_within [prf, in mathcomp.analysis.normedtype]
    cvg_at_rightE [prf, in mathcomp.analysis.normedtype]
    cvg_at_rightE [prf, in mathcomp.analysis.derive]
    cvg_at_rightNP [prf, in mathcomp.analysis.normedtype]
    cvg_at_rightP [prf, in mathcomp.analysis.realfun]
    cvg_ball [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    cvg_ball2P [prf, in mathcomp.analysis.topology_theory.product_topology]
    cvg_ballP [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    cvg_ballPpos [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
    cvg_bounded [prf, in mathcomp.analysis.normedtype]
    cvg_cauchy [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    cvg_centern [prf, in mathcomp.analysis.sequences]
    cvg_centerr [prf, in mathcomp.analysis.realfun]
    cvg_close [prf, in mathcomp.analysis.separation_axioms]
    cvg_closeP [prf, in mathcomp.analysis.separation_axioms]
    cvg_cluster [prf, in mathcomp.analysis.topology_theory.compact]
    cvg_comp [prf, in mathcomp.classical.filter]
    cvg_comp2 [prf, in mathcomp.classical.filter]
    cvg_comp_shift [prf, in mathcomp.analysis.normedtype]
    cvg_composition_field.F [var, in mathcomp.analysis.normedtype]
    cvg_composition_field.FF [var, in mathcomp.analysis.normedtype]
    cvg_composition_field.K [var, in mathcomp.analysis.normedtype]
    cvg_composition_field.T [var, in mathcomp.analysis.normedtype]
    cvg_composition_field_proper.F [var, in mathcomp.analysis.normedtype]
    cvg_composition_field_proper.FF [var, in mathcomp.analysis.normedtype]
    cvg_composition_field_proper.K [var, in mathcomp.analysis.normedtype]
    cvg_composition_field_proper.T [var, in mathcomp.analysis.normedtype]
    cvg_composition_normed.F [var, in mathcomp.analysis.normedtype]
    cvg_composition_normed.FF [var, in mathcomp.analysis.normedtype]
    cvg_composition_normed.K [var, in mathcomp.analysis.normedtype]
    cvg_composition_normed.T [var, in mathcomp.analysis.normedtype]
    cvg_composition_normed.V [var, in mathcomp.analysis.normedtype]
    cvg_composition_pseudometric.F [var, in mathcomp.analysis.normedtype]
    cvg_composition_pseudometric.FF [var, in mathcomp.analysis.normedtype]
    cvg_composition_pseudometric.K [var, in mathcomp.analysis.normedtype]
    cvg_composition_pseudometric.T [var, in mathcomp.analysis.normedtype]
    cvg_composition_pseudometric.V [var, in mathcomp.analysis.normedtype]
    cvg_cos_coeff' [prf, in mathcomp.analysis.trigo]
    cvg_cst [prf, in mathcomp.analysis.topology_theory.topology_structure]
    cvg_dist2P [abbrev, in mathcomp.analysis.normedtype]
    cvg_distP [abbrev, in mathcomp.analysis.normedtype]
    cvg_distW [abbrev, in mathcomp.analysis.normedtype]
    cvg_divnr [prf, in mathcomp.analysis.topology_theory.nat_topology]
    cvg_EFin [prf, in mathcomp.analysis.normedtype]
    cvg_einfs [prf, in mathcomp.analysis.sequences]
    cvg_einfs_sup [prf, in mathcomp.analysis.sequences]
    cvg_entourage [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    cvg_entourageP [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    cvg_eq [prf, in mathcomp.analysis.separation_axioms]
    cvg_ereal_loc_seq [prf, in mathcomp.analysis.ereal]
    cvg_esups [prf, in mathcomp.analysis.sequences]
    cvg_esups_inf [prf, in mathcomp.analysis.sequences]
    cvg_ex [prf, in mathcomp.classical.filter]
    cvg_exp_coeff [prf, in mathcomp.analysis.sequences]
    cvg_expr [prf, in mathcomp.analysis.sequences]
    cvg_fct_entourageP [prf, in mathcomp.analysis.function_spaces]
    cvg_fin.filter.F [var, in mathcomp.analysis.normedtype]
    cvg_fin.filter.FF [var, in mathcomp.analysis.normedtype]
    cvg_fin.limit.f [var, in mathcomp.analysis.normedtype]
    cvg_fin.limit.F [var, in mathcomp.analysis.normedtype]
    cvg_fin.limit.FF [var, in mathcomp.analysis.normedtype]
    cvg_fin.limit.I [var, in mathcomp.analysis.normedtype]
    cvg_fin.R [var, in mathcomp.analysis.normedtype]
    cvg_fmap [prf, in mathcomp.analysis.topology_theory.topology_structure]
    cvg_fmap2 [prf, in mathcomp.analysis.topology_theory.topology_structure]
    cvg_fst [prf, in mathcomp.classical.filter]
    cvg_geometric [prf, in mathcomp.analysis.sequences]
    cvg_geometric_eseries_half [prf, in mathcomp.analysis.sequences]
    cvg_geometric_series [prf, in mathcomp.analysis.sequences]
    cvg_geometric_series_half [prf, in mathcomp.analysis.sequences]
    cvg_gt_ge [abbrev, in mathcomp.analysis.normedtype]
    cvg_harmonic [prf, in mathcomp.analysis.sequences]
    cvg_has_inf [prf, in mathcomp.analysis.sequences]
    cvg_has_sup [prf, in mathcomp.analysis.sequences]
    cvg_has_ub [prf, in mathcomp.analysis.sequences]
    cvg_id [prf, in mathcomp.classical.filter]
    cvg_image [prf, in mathcomp.analysis.topology_theory.weak_topology]
    cvg_in_ex [prf, in mathcomp.classical.filter]
    cvg_in_toP [prf, in mathcomp.classical.filter]
    cvg_indic [prf, in mathcomp.analysis.numfun]
    cvg_infs [prf, in mathcomp.analysis.sequences]
    cvg_infs_sup [prf, in mathcomp.analysis.sequences]
    cvg_infty_numField.cvgrNyPnum [var, in mathcomp.analysis.normedtype]
    cvg_infty_numField.cvgryPnum [var, in mathcomp.analysis.normedtype]
    cvg_infty_numField.F [var, in mathcomp.analysis.normedtype]
    cvg_infty_numField.FF [var, in mathcomp.analysis.normedtype]
    cvg_infty_numField.R [var, in mathcomp.analysis.normedtype]
    cvg_infty_numField.T [var, in mathcomp.analysis.normedtype]
    cvg_infty_realField.f [var, in mathcomp.analysis.normedtype]
    cvg_infty_realField.F [var, in mathcomp.analysis.normedtype]
    cvg_infty_realField.FF [var, in mathcomp.analysis.normedtype]
    cvg_infty_realField.R [var, in mathcomp.analysis.normedtype]
    cvg_infty_realField.T [var, in mathcomp.analysis.normedtype]
    cvg_inNpoint [prf, in mathcomp.classical.filter]
    cvg_inP [prf, in mathcomp.classical.filter]
    cvg_is_fine [prf, in mathcomp.analysis.normedtype]
    cvg_lim [prf, in mathcomp.analysis.separation_axioms]
    cvg_lim_einf_sup [abbrev, in mathcomp.analysis.sequences]
    cvg_lim_infE [abbrev, in mathcomp.analysis.sequences]
    cvg_lim_supE [abbrev, in mathcomp.analysis.sequences]
    cvg_limn_einf_sup [prf, in mathcomp.analysis.sequences]
    cvg_limn_inf_sup [prf, in mathcomp.analysis.sequences]
    cvg_limn_infE [prf, in mathcomp.analysis.sequences]
    cvg_limn_supE [prf, in mathcomp.analysis.sequences]
    cvg_lt_le_ [abbrev, in mathcomp.analysis.normedtype]
    cvg_map_lim [abbrev, in mathcomp.analysis.separation_axioms]
    cvg_monotone_convergence [prf, in mathcomp.analysis.lebesgue_integral]
    cvg_mulnl [prf, in mathcomp.analysis.topology_theory.nat_topology]
    cvg_mulnr [prf, in mathcomp.analysis.topology_theory.nat_topology]
    cvg_mx_entourageP [prf, in mathcomp.analysis.topology_theory.matrix_topology]
    cvg_nbhsP [prf, in mathcomp.analysis.realfun]
    cvg_near_const [prf, in mathcomp.classical.filter]
    cvg_near_cst [prf, in mathcomp.analysis.topology_theory.topology_structure]
    cvg_ninftyP [prf, in mathcomp.analysis.realfun]
    cvg_nnesum [prf, in mathcomp.analysis.normedtype]
    cvg_nnsfun_approx [prf, in mathcomp.analysis.lebesgue_integral]
    cvg_norm [prf, in mathcomp.analysis.normedtype]
    cvg_nseries_near [prf, in mathcomp.analysis.sequences]
    cvg_pair [prf, in mathcomp.classical.filter]
    cvg_patch [prf, in mathcomp.analysis.normedtype]
    cvg_pinftyP [prf, in mathcomp.analysis.realfun]
    cvg_prod [prf, in mathcomp.classical.filter]
    cvg_refl [prf, in mathcomp.classical.filter]
    cvg_restrict [prf, in mathcomp.analysis.sequences]
    cvg_seq_bounded [prf, in mathcomp.analysis.normedtype]
    +oo [not, in mathcomp.analysis.normedtype] (no scope)
    cvg_seq_bounded.K [var, in mathcomp.analysis.normedtype]
    cvg_series_bounded [prf, in mathcomp.analysis.sequences]
    cvg_series_cvg_0 [prf, in mathcomp.analysis.sequences]
    cvg_series_cvg_series_group [prf, in mathcomp.analysis.trigo]
    cvg_shiftn [prf, in mathcomp.analysis.sequences]
    cvg_shiftr [prf, in mathcomp.analysis.realfun]
    cvg_shiftS [prf, in mathcomp.analysis.sequences]
    cvg_sigL [prf, in mathcomp.analysis.function_spaces]
    cvg_sin_coeff' [prf, in mathcomp.analysis.trigo]
    cvg_snd [prf, in mathcomp.classical.filter]
    cvg_sub0 [prf, in mathcomp.analysis.normedtype]
    cvg_subnr [prf, in mathcomp.analysis.topology_theory.nat_topology]
    cvg_sup [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    cvg_sups [prf, in mathcomp.analysis.sequences]
    cvg_sups_inf [prf, in mathcomp.analysis.sequences]
    cvg_switch [prf, in mathcomp.analysis.function_spaces]
    Cvg_switch.T1 [var, in mathcomp.analysis.function_spaces]
    Cvg_switch.T2 [var, in mathcomp.analysis.function_spaces]
    cvg_switch_1 [prf, in mathcomp.analysis.function_spaces]
    cvg_switch_2 [prf, in mathcomp.analysis.function_spaces]
    cvg_to [def, in mathcomp.classical.filter]
    cvg_to_0_linear [prf, in mathcomp.analysis.sequences]
    cvg_to_comp_2 [def, in mathcomp.classical.filter]
    cvg_toi_locally [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    cvg_toi_locally_close [def, in mathcomp.analysis.separation_axioms]
    cvg_toP [prf, in mathcomp.classical.filter]
    cvg_trans [prf, in mathcomp.classical.filter]
    cvg_uniform_set0 [prf, in mathcomp.analysis.function_spaces]
    cvg_uniformU [prf, in mathcomp.analysis.function_spaces]
    cvg_unique [prf, in mathcomp.analysis.separation_axioms]
    cvg_within [prf, in mathcomp.classical.filter]
    cvg_within_filter [prf, in mathcomp.analysis.topology_theory.topology_structure]
    cvg_zero [prf, in mathcomp.analysis.normedtype]
    cvgB [prf, in mathcomp.analysis.normedtype]
    cvgD [prf, in mathcomp.analysis.normedtype]
    cvge_at_leftP [prf, in mathcomp.analysis.realfun]
    cvge_at_rightP [prf, in mathcomp.analysis.realfun]
    cvge_ge [prf, in mathcomp.analysis.normedtype]
    cvge_harmonic [prf, in mathcomp.analysis.sequences]
    cvge_le [prf, in mathcomp.analysis.normedtype]
    cvge_sub0 [prf, in mathcomp.analysis.normedtype]
    cvge_to_ge [prf, in mathcomp.analysis.normedtype]
    cvge_to_le [prf, in mathcomp.analysis.normedtype]
    cvgeB [prf, in mathcomp.analysis.normedtype]
    cvgeD [prf, in mathcomp.analysis.normedtype]
    cvgeM [prf, in mathcomp.analysis.normedtype]
    cvgeMl [prf, in mathcomp.analysis.normedtype]
    cvgeMr [prf, in mathcomp.analysis.normedtype]
    cvgeN [prf, in mathcomp.analysis.normedtype]
    cvgeNP [prf, in mathcomp.analysis.normedtype]
    cvgeNy_le [prf, in mathcomp.analysis.normedtype]
    cvgeNy_ler [prf, in mathcomp.analysis.normedtype]
    cvgeNy_lt [prf, in mathcomp.analysis.normedtype]
    cvgeNy_ltr [prf, in mathcomp.analysis.normedtype]
    cvgenyP [prf, in mathcomp.analysis.normedtype]
    cvgeNyPle [prf, in mathcomp.analysis.normedtype]
    cvgeNyPleNy [prf, in mathcomp.analysis.normedtype]
    cvgeNyPler [prf, in mathcomp.analysis.normedtype]
    cvgeNyPlt [prf, in mathcomp.analysis.normedtype]
    cvgeNyPltNy [prf, in mathcomp.analysis.normedtype]
    cvgeNyPltr [prf, in mathcomp.analysis.normedtype]
    cvgerNyP [prf, in mathcomp.analysis.normedtype]
    cvgeryP [prf, in mathcomp.analysis.normedtype]
    cvgey_ge [prf, in mathcomp.analysis.normedtype]
    cvgey_ger [prf, in mathcomp.analysis.normedtype]
    cvgey_gt [prf, in mathcomp.analysis.normedtype]
    cvgey_gtr [prf, in mathcomp.analysis.normedtype]
    cvgeyPge [prf, in mathcomp.analysis.normedtype]
    cvgeyPger [prf, in mathcomp.analysis.normedtype]
    cvgeyPgey [prf, in mathcomp.analysis.normedtype]
    cvgeyPgt [prf, in mathcomp.analysis.normedtype]
    cvgeyPgtr [prf, in mathcomp.analysis.normedtype]
    cvgeyPgty [prf, in mathcomp.analysis.normedtype]
    cvgi_app [prf, in mathcomp.classical.filter]
    cvgi_ball [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    cvgi_ballP [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    cvgi_close [prf, in mathcomp.analysis.separation_axioms]
    cvgi_comp [prf, in mathcomp.classical.filter]
    cvgi_lim [prf, in mathcomp.analysis.separation_axioms]
    cvgi_map_lim [abbrev, in mathcomp.analysis.separation_axioms]
    cvgi_unique [prf, in mathcomp.analysis.separation_axioms]
    cvgM [prf, in mathcomp.analysis.normedtype]
    cvgMl [prf, in mathcomp.analysis.normedtype]
    cvgMn [prf, in mathcomp.analysis.normedtype]
    cvgMr [prf, in mathcomp.analysis.normedtype]
    cvgn [abbrev, in mathcomp.classical.filter]
    cvgN [prf, in mathcomp.analysis.normedtype]
    cvgn_expR [prf, in mathcomp.analysis.exp]
    cvgNeNy [prf, in mathcomp.analysis.normedtype]
    cvgNey [prf, in mathcomp.analysis.normedtype]
    cvgNP [prf, in mathcomp.analysis.normedtype]
    cvgNpoint [prf, in mathcomp.classical.filter]
    cvgNrNy [prf, in mathcomp.analysis.normedtype]
    cvgNry [prf, in mathcomp.analysis.normedtype]
    cvgNy_einfs [prf, in mathcomp.analysis.sequences]
    cvgNy_esups [prf, in mathcomp.analysis.sequences]
    cvgNy_lim_einf_sup [abbrev, in mathcomp.analysis.sequences]
    cvgNy_limn_einf_sup [prf, in mathcomp.analysis.sequences]
    cvgnyPge [prf, in mathcomp.analysis.topology_theory.nat_topology]
    cvgnyPgey [prf, in mathcomp.analysis.topology_theory.nat_topology]
    cvgnyPgt [prf, in mathcomp.analysis.topology_theory.nat_topology]
    cvgnyPgty [prf, in mathcomp.analysis.topology_theory.nat_topology]
    cvgP [prf, in mathcomp.classical.filter]
    cvgPninfty_lt [abbrev, in mathcomp.analysis.sequences]
    cvgPninfty_lt_near [abbrev, in mathcomp.analysis.sequences]
    cvgPninfty_near [abbrev, in mathcomp.analysis.sequences]
    cvgPpinfty_lt [abbrev, in mathcomp.analysis.sequences]
    cvgPpinfty_lt_near [abbrev, in mathcomp.analysis.sequences]
    cvgPpinfty_near [abbrev, in mathcomp.analysis.sequences]
    cvgr0_norm_le [prf, in mathcomp.analysis.normedtype]
    cvgr0_norm_lt [prf, in mathcomp.analysis.normedtype]
    cvgr0Pnorm_le [prf, in mathcomp.analysis.normedtype]
    cvgr0Pnorm_lep [prf, in mathcomp.analysis.normedtype]
    cvgr0Pnorm_lt [prf, in mathcomp.analysis.normedtype]
    cvgr0Pnorm_ltp [prf, in mathcomp.analysis.normedtype]
    cvgr2dist_lt [prf, in mathcomp.analysis.normedtype]
    cvgr2dist_ltP [prf, in mathcomp.analysis.normedtype]
    cvgr_dist_le [prf, in mathcomp.analysis.normedtype]
    cvgr_dist_lt [prf, in mathcomp.analysis.normedtype]
    cvgr_distC_le [prf, in mathcomp.analysis.normedtype]
    cvgr_distC_lt [prf, in mathcomp.analysis.normedtype]
    cvgr_dnbhsP [prf, in mathcomp.analysis.realfun]
    cvgr_expR [prf, in mathcomp.analysis.exp]
    cvgr_ge [prf, in mathcomp.analysis.normedtype]
    cvgr_gt [prf, in mathcomp.analysis.normedtype]
    cvgr_le [prf, in mathcomp.analysis.normedtype]
    cvgr_lt [prf, in mathcomp.analysis.normedtype]
    cvgr_neq0 [prf, in mathcomp.analysis.normedtype]
    cvgr_norm_ge [prf, in mathcomp.analysis.normedtype]
    cvgr_norm_geNy [prf, in mathcomp.analysis.normedtype]
    cvgr_norm_gt [prf, in mathcomp.analysis.normedtype]
    cvgr_norm_gtNy [prf, in mathcomp.analysis.normedtype]
    cvgr_norm_le [prf, in mathcomp.analysis.normedtype]
    cvgr_norm_ley [prf, in mathcomp.analysis.normedtype]
    cvgr_norm_lt [prf, in mathcomp.analysis.normedtype]
    cvgr_norm_lty [prf, in mathcomp.analysis.normedtype]
    cvgr_to_ge [prf, in mathcomp.analysis.normedtype]
    cvgr_to_le [prf, in mathcomp.analysis.normedtype]
    cvgrNy_le [prf, in mathcomp.analysis.normedtype]
    cvgrNy_ler [prf, in mathcomp.analysis.normedtype]
    cvgrNy_lt [prf, in mathcomp.analysis.normedtype]
    cvgrNy_ltr [prf, in mathcomp.analysis.normedtype]
    cvgrnyP [prf, in mathcomp.analysis.normedtype]
    cvgrNyPle [prf, in mathcomp.analysis.normedtype]
    cvgrNyPleNy [prf, in mathcomp.analysis.normedtype]
    cvgrNyPler [prf, in mathcomp.analysis.normedtype]
    cvgrNyPlt [prf, in mathcomp.analysis.normedtype]
    cvgrNyPltNy [prf, in mathcomp.analysis.normedtype]
    cvgrNyPltr [prf, in mathcomp.analysis.normedtype]
    cvgrPdist_le [prf, in mathcomp.analysis.normedtype]
    cvgrPdist_lep [prf, in mathcomp.analysis.normedtype]
    cvgrPdist_lt [prf, in mathcomp.analysis.normedtype]
    cvgrPdist_ltp [prf, in mathcomp.analysis.normedtype]
    cvgrPdistC_le [prf, in mathcomp.analysis.normedtype]
    cvgrPdistC_lep [prf, in mathcomp.analysis.normedtype]
    cvgrPdistC_lt [prf, in mathcomp.analysis.normedtype]
    cvgrPdistC_ltp [prf, in mathcomp.analysis.normedtype]
    cvgrVNy [prf, in mathcomp.analysis.normedtype]
    cvgrVy [prf, in mathcomp.analysis.normedtype]
    cvgry_ge [prf, in mathcomp.analysis.normedtype]
    cvgry_ger [prf, in mathcomp.analysis.normedtype]
    cvgry_gt [prf, in mathcomp.analysis.normedtype]
    cvgry_gtr [prf, in mathcomp.analysis.normedtype]
    cvgryPge [prf, in mathcomp.analysis.normedtype]
    cvgryPger [prf, in mathcomp.analysis.normedtype]
    cvgryPgey [prf, in mathcomp.analysis.normedtype]
    cvgryPgt [prf, in mathcomp.analysis.normedtype]
    cvgryPgtr [prf, in mathcomp.analysis.normedtype]
    cvgryPgty [prf, in mathcomp.analysis.normedtype]
    cvgV [prf, in mathcomp.analysis.normedtype]
    cvgVP [prf, in mathcomp.analysis.normedtype]
    cvgx_close [prf, in mathcomp.analysis.separation_axioms]
    cvgy_atan [prf, in mathcomp.analysis.trigo]
    cvgy_einfs [prf, in mathcomp.analysis.sequences]
    cvgy_esups [prf, in mathcomp.analysis.sequences]
    cvgyNP [prf, in mathcomp.analysis.normedtype]
    cvgZ [prf, in mathcomp.analysis.normedtype]
    cvgZl [prf, in mathcomp.analysis.normedtype]
    cvgZr [prf, in mathcomp.analysis.normedtype]
    czero [def, in mathcomp.analysis.charge]
    Generated by a fork of coq2html