Files

  • mathcomp

    • Top

    'S' (Global Index)

    FilesABCDEFGHIJKLMNOPQRSTUVWXYZ_*
    DefinitionsABCDEFGHIJKLMNOPQRSTUVWXYZ_*
    LemmasABCDEFGHIJKLMNOPQRSTUVWXYZ_*
    AbbreviationsABCDEFGHIJKLMNOPQRSTUVWXYZ_*
    Global IndexABCDEFGHIJKLMNOPQRSTUVWXYZ_*

    S

    S [abbrev, in mathcomp.analysis.topology_theory.weak_topology]
    S [abbrev, in mathcomp.analysis.topology_theory.supremum_topology]
    S [abbrev, in mathcomp.analysis.separation_axioms]
    s_finite [def, in mathcomp.analysis.measure]
    salgebra_ereal.G [var, in mathcomp.analysis.lebesgue_measure]
    salgebra_ereal.measurableR [var, in mathcomp.analysis.lebesgue_measure]
    salgebra_ereal.R [var, in mathcomp.analysis.lebesgue_measure]
    salgebra_R_ssets.emeasurable_itv_bndy [var, in mathcomp.analysis.lebesgue_measure]
    salgebra_R_ssets.emeasurable_itv_Nybnd [var, in mathcomp.analysis.lebesgue_measure]
    salgebra_R_ssets.R [var, in mathcomp.analysis.lebesgue_measure]
    salgebraType [abbrev, in mathcomp.analysis.measure]
    same_connected_component [prf, in mathcomp.analysis.topology_theory.connected]
    same_prefix [def, in mathcomp.classical.classical_orders]
    same_prefix0 [prf, in mathcomp.classical.classical_orders]
    same_prefix_leq [prf, in mathcomp.classical.classical_orders]
    same_prefix_refl [prf, in mathcomp.classical.classical_orders]
    same_prefix_sym [prf, in mathcomp.classical.classical_orders]
    same_prefix_trans [prf, in mathcomp.classical.classical_orders]
    scale [abbrev, in mathcomp.analysis.measure]
    scale_ball [def, in mathcomp.analysis.normedtype]
    scale_ball0 [prf, in mathcomp.analysis.normedtype]
    scale_ball1 [prf, in mathcomp.analysis.normedtype]
    scale_ball_set0 [prf, in mathcomp.analysis.normedtype]
    scale_ballE [prf, in mathcomp.analysis.normedtype]
    scale_continuous [def, in mathcomp.analysis.tvs]
    scale_continuous [prf, in mathcomp.analysis.normedtype]
    scale_fimfun [def, in mathcomp.analysis.numfun]
    scale_littleo [def, in mathcomp.analysis.landau]
    scale_littleo_subproof [prf, in mathcomp.analysis.landau]
    scale_mfun [def, in mathcomp.analysis.lebesgue_integral]
    scale_nnsfun [def, in mathcomp.analysis.lebesgue_integral]
    scale_sfun [def, in mathcomp.analysis.lebesgue_integral]
    scalel_continuous [prf, in mathcomp.analysis.normedtype]
    scaleo [prf, in mathcomp.analysis.landau]
    scaleolx [prf, in mathcomp.analysis.landau]
    scaleox [prf, in mathcomp.analysis.landau]
    scaler_continuous [prf, in mathcomp.analysis.normedtype]
    scalrfctE [prf, in mathcomp.classical.functions]
    sdrop [def, in mathcomp.analysis.sequences]
    sdrop.d [var, in mathcomp.analysis.sequences]
    sdrop.R [var, in mathcomp.analysis.sequences]
    second_countable [def, in mathcomp.analysis.topology_theory.topology_structure]
    second_derivative_convex [prf, in mathcomp.analysis.convex]
    section.T1 [var, in mathcomp.classical.classical_sets]
    section.T2 [var, in mathcomp.classical.classical_sets]
    sedDI_closedP [prf, in mathcomp.analysis.measure]
    segment.R [var, in mathcomp.analysis.normedtype]
    segment_can_continuous [prf, in mathcomp.analysis.realfun]
    segment_can_ge [prf, in mathcomp.analysis.realfun]
    segment_can_ge_continuous [prf, in mathcomp.analysis.realfun]
    segment_can_le [prf, in mathcomp.analysis.realfun]
    segment_can_le_continuous [prf, in mathcomp.analysis.realfun]
    segment_can_mono [prf, in mathcomp.analysis.realfun]
    segment_compact [prf, in mathcomp.analysis.normedtype]
    segment_connected [prf, in mathcomp.analysis.normedtype]
    segment_continuous_can_sym [prf, in mathcomp.analysis.realfun]
    segment_continuous_ge_can_sym [prf, in mathcomp.analysis.realfun]
    segment_continuous_ge_surjective [prf, in mathcomp.analysis.realfun]
    segment_continuous_inj_ge [prf, in mathcomp.analysis.realfun]
    segment_continuous_inj_le [prf, in mathcomp.analysis.realfun]
    segment_continuous_le_can_sym [prf, in mathcomp.analysis.realfun]
    segment_continuous_le_surjective [prf, in mathcomp.analysis.realfun]
    segment_continuous_surjective [prf, in mathcomp.analysis.realfun]
    segment_dec_surj_continuous [prf, in mathcomp.analysis.realfun]
    segment_inc_surj_continuous [prf, in mathcomp.analysis.realfun]
    segment_mono_surj_continuous [prf, in mathcomp.analysis.realfun]
    self_sub [def, in mathcomp.analysis.normedtype]
    selfFiltered [mod, in mathcomp.classical.filter]
    selfFiltered.axioms_ [rec, in mathcomp.classical.filter]
    selfFiltered.Exports [mod, in mathcomp.classical.filter]
    selfFiltered.identity_builder [def, in mathcomp.classical.filter]
    selfFiltered.phant_axioms [def, in mathcomp.classical.filter]
    selfFiltered.phant_Build [def, in mathcomp.classical.filter]
    selfFiltered.selfFiltered.T [var, in mathcomp.classical.filter]
    selfPbij [abbrev, in mathcomp.classical.functions]
    semi_additive [def, in mathcomp.analysis.measure]
    semi_additive2 [def, in mathcomp.analysis.measure]
    semi_additive2E [prf, in mathcomp.analysis.measure]
    semi_additiveE [prf, in mathcomp.analysis.measure]
    semi_additiveW [prf, in mathcomp.analysis.measure]
    semi_measurableD [def, in mathcomp.analysis.measure]
    semi_setD_closed [def, in mathcomp.analysis.measure]
    semi_sigma_additive [def, in mathcomp.analysis.measure]
    semi_sigma_additive_elebesgue_measure [prf, in mathcomp.analysis.lebesgue_measure]
    semi_sigma_additive_is_additive [prf, in mathcomp.analysis.measure]
    semi_sigma_additive_nng_induced [prf, in mathcomp.analysis.charge]
    semi_sigma_additiveE [prf, in mathcomp.analysis.measure]
    semiring_sigma_additive [prf, in mathcomp.analysis.measure]
    SemiRingOfSets [mod, in mathcomp.analysis.measure]
    SemiRingOfSets.axioms_ [rec, in mathcomp.analysis.measure]
    SemiRingOfSets.choice_hasChoice_mixin [proj, in mathcomp.analysis.measure]
    SemiRingOfSets.class [proj, in mathcomp.analysis.measure]
    SemiRingOfSets.classical_sets_isPointed_mixin [proj, in mathcomp.analysis.measure]
    SemiRingOfSets.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.measure]
    SemiRingOfSets.Exports [mod, in mathcomp.analysis.measure]
    SemiRingOfSets.Exports.measure_SemiRingOfSets__to__choice_Choice [def, in mathcomp.analysis.measure]
    SemiRingOfSets.Exports.measure_SemiRingOfSets__to__classical_sets_Pointed [def, in mathcomp.analysis.measure]
    SemiRingOfSets.Exports.measure_SemiRingOfSets__to__eqtype_Equality [def, in mathcomp.analysis.measure]
    SemiRingOfSets.Exports.measure_SemiRingOfSets_class__to__choice_Choice_class [def, in mathcomp.analysis.measure]
    SemiRingOfSets.Exports.measure_SemiRingOfSets_class__to__classical_sets_Pointed_class [def, in mathcomp.analysis.measure]
    SemiRingOfSets.Exports.measure_SemiRingOfSets_class__to__eqtype_Equality_class [def, in mathcomp.analysis.measure]
    SemiRingOfSets.measure_isSemiRingOfSets_mixin [proj, in mathcomp.analysis.measure]
    SemiRingOfSets.pack_ [def, in mathcomp.analysis.measure]
    SemiRingOfSets.phant_clone [def, in mathcomp.analysis.measure]
    SemiRingOfSets.phant_on_ [def, in mathcomp.analysis.measure]
    SemiRingOfSets.sort [proj, in mathcomp.analysis.measure]
    SemiRingOfSets.type [rec, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets [mod, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.axioms_ [rec, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.Exports [mod, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.identity_builder [def, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.measurableU [proj, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.phant_axioms [def, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.phant_Build [def, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.SemiRingOfSets_isRingOfSets.d [var, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.SemiRingOfSets_isRingOfSets.local_mixin_choice_hasChoice [var, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.SemiRingOfSets_isRingOfSets.local_mixin_classical_sets_isPointed [var, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.SemiRingOfSets_isRingOfSets.local_mixin_eqtype_hasDecEq [var, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.SemiRingOfSets_isRingOfSets.local_mixin_measure_isSemiRingOfSets [var, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.SemiRingOfSets_isRingOfSets.T [var, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.SemiRingOfSets_isRingOfSets_T__canonical__choice_Choice [def, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.SemiRingOfSets_isRingOfSets_T__canonical__classical_sets_Pointed [def, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.SemiRingOfSets_isRingOfSets_T__canonical__eqtype_Equality [def, in mathcomp.analysis.measure]
    SemiRingOfSets_isRingOfSets.SemiRingOfSets_isRingOfSets_T__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
    SemiRingOfSetsElpiOperations [mod, in mathcomp.analysis.measure]
    separable [prf, in mathcomp.experimental_reals.realseq]
    separable_le [prf, in mathcomp.experimental_reals.realseq]
    separate_points_from_closed [def, in mathcomp.analysis.function_spaces]
    separated [def, in mathcomp.analysis.topology_theory.connected]
    separated_closed_ball_countable [prf, in mathcomp.analysis.normedtype]
    separated_disjoint [prf, in mathcomp.analysis.topology_theory.connected]
    separated_open_countable [prf, in mathcomp.analysis.topology_theory.num_topology]
    separatedC [prf, in mathcomp.analysis.topology_theory.connected]
    separation_axioms [file, in mathcomp.analysis.separation_axioms]
    separation_axioms_sup_pseudometric__canonical__choice_Choice [def, in mathcomp.analysis.separation_axioms]
    separation_axioms_sup_pseudometric__canonical__eqtype_Equality [def, in mathcomp.analysis.separation_axioms]
    separation_axioms_sup_pseudometric__canonical__filter_Filtered [def, in mathcomp.analysis.separation_axioms]
    separation_axioms_sup_pseudometric__canonical__filter_Nbhs [def, in mathcomp.analysis.separation_axioms]
    separation_axioms_sup_pseudometric__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.separation_axioms]
    separation_axioms_sup_pseudometric__canonical__topology_structure_Topological [def, in mathcomp.analysis.separation_axioms]
    separation_axioms_sup_pseudometric__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.separation_axioms]
    seq_psume_eq0 [prf, in mathcomp.reals.constructive_ereal]
    seqD [def, in mathcomp.analysis.sequences]
    seqD.T [var, in mathcomp.analysis.sequences]
    seqDU [def, in mathcomp.analysis.sequences]
    seqDU.T [var, in mathcomp.analysis.sequences]
    seqDU_bigcup_eq [prf, in mathcomp.analysis.sequences]
    seqDU_seqD [prf, in mathcomp.analysis.sequences]
    seqDUIE [prf, in mathcomp.analysis.sequences]
    SeqLimTh.R [var, in mathcomp.experimental_reals.realseq]
    sequence [def, in mathcomp.analysis.sequences]
    sequence_measure.d [var, in mathcomp.analysis.lebesgue_integral]
    sequence_measure.m [var, in mathcomp.analysis.lebesgue_integral]
    sequence_measure.m_ [var, in mathcomp.analysis.lebesgue_integral]
    sequence_measure.R [var, in mathcomp.analysis.lebesgue_integral]
    sequence_measure.T [var, in mathcomp.analysis.lebesgue_integral]
    SequenceLim.R [var, in mathcomp.experimental_reals.realseq]
    sequences [file, in mathcomp.analysis.sequences]
    sequences_ereal.cvg_eseries.R [var, in mathcomp.analysis.sequences]
    sequences_ereal.cvg_eseries.u_ [var, in mathcomp.analysis.sequences]
    sequences_ereal.ereal_series.f [var, in mathcomp.analysis.sequences]
    sequences_ereal.ereal_series.R [var, in mathcomp.analysis.sequences]
    sequences_ereal.lim_shift_cst [var, in mathcomp.analysis.sequences]
    sequences_ereal.nneseries_split.near_eq_lim [var, in mathcomp.analysis.sequences]
    sequences_ereal_realDomainType.T [var, in mathcomp.analysis.sequences]
    sequences_expR__canonical__lebesgue_integral_MeasurableFun [def, in mathcomp.analysis.lebesgue_integral]
    sequences_patched.NatShift.N [var, in mathcomp.analysis.sequences]
    sequences_patched.NatShift.V [var, in mathcomp.analysis.sequences]
    sequences_patched.V [var, in mathcomp.analysis.sequences]
    sequences_R_lemmas.R [var, in mathcomp.analysis.sequences]
    sequences_R_lemmas_realFieldType.R [var, in mathcomp.analysis.sequences]
    series [def, in mathcomp.analysis.sequences]
    series_addn [prf, in mathcomp.analysis.sequences]
    series_cos_coeff0 [prf, in mathcomp.analysis.trigo]
    series_exp_coeff0 [prf, in mathcomp.analysis.sequences]
    series_le_cvg [prf, in mathcomp.analysis.sequences]
    series_patched.K [var, in mathcomp.analysis.sequences]
    series_patched.N [var, in mathcomp.analysis.sequences]
    series_patched.V [var, in mathcomp.analysis.sequences]
    series_sin_coeff0 [prf, in mathcomp.analysis.trigo]
    seriesD [prf, in mathcomp.analysis.sequences]
    seriesEnat [prf, in mathcomp.analysis.sequences]
    seriesEord [prf, in mathcomp.analysis.sequences]
    seriesK [prf, in mathcomp.analysis.sequences]
    seriesN [prf, in mathcomp.analysis.sequences]
    seriesS [prf, in mathcomp.analysis.sequences]
    seriesSB [prf, in mathcomp.analysis.sequences]
    seriesSr [prf, in mathcomp.analysis.sequences]
    seriesZ [prf, in mathcomp.analysis.sequences]
    sesqui [def, in mathcomp.analysis.forms]
    sesqui_key [prf, in mathcomp.analysis.forms]
    sesqui_keyed [def, in mathcomp.analysis.forms]
    sesquiE [prf, in mathcomp.analysis.forms]
    .-sesqui [not, in mathcomp.analysis.forms] (no scope)
    '[ , ] [not, in mathcomp.analysis.forms] (in ring_scope)
    '[ ] [not, in mathcomp.analysis.forms] (in ring_scope)
    ^_|_ [not, in mathcomp.analysis.forms] (in ring_scope)
    _|_ [not, in mathcomp.analysis.forms] (in ring_scope)
    Sesquilinear.Def.eps_theta [var, in mathcomp.analysis.forms]
    Sesquilinear.eps [var, in mathcomp.analysis.forms]
    Sesquilinear.M [var, in mathcomp.analysis.forms]
    Sesquilinear.M_sesqui [var, in mathcomp.analysis.forms]
    Sesquilinear.n [var, in mathcomp.analysis.forms]
    Sesquilinear.R [var, in mathcomp.analysis.forms]
    Sesquilinear.theta [var, in mathcomp.analysis.forms]
    Sesquilinear.thetaK [var, in mathcomp.analysis.forms]
    sesquiP [prf, in mathcomp.analysis.forms]
    set [def, in mathcomp.classical.classical_sets]
    set0 [def, in mathcomp.classical.classical_sets]
    set0D [prf, in mathcomp.classical.classical_sets]
    set0fun [prf, in mathcomp.classical.classical_sets]
    set0fun_inj [prf, in mathcomp.classical.functions]
    set0I [prf, in mathcomp.classical.classical_sets]
    set0M [abbrev, in mathcomp.classical.classical_sets]
    set0P [prf, in mathcomp.classical.classical_sets]
    set0U [prf, in mathcomp.classical.classical_sets]
    set0X [prf, in mathcomp.classical.classical_sets]
    set0Y [prf, in mathcomp.classical.classical_sets]
    set1 [def, in mathcomp.classical.classical_sets]
    set1_bigcap_oc [prf, in mathcomp.reals.real_interval]
    set1I [prf, in mathcomp.classical.classical_sets]
    set_andb [prf, in mathcomp.classical.classical_sets]
    set_bij [def, in mathcomp.classical.functions]
    set_bij00 [prf, in mathcomp.classical.functions]
    set_bij_basic_lemmas.aT [var, in mathcomp.classical.functions]
    set_bij_basic_lemmas.rT [var, in mathcomp.classical.functions]
    set_bij_bijfun [def, in mathcomp.classical.functions]
    set_bij_comp [prf, in mathcomp.classical.functions]
    set_bij_homo [prf, in mathcomp.classical.functions]
    set_bij_inj [prf, in mathcomp.classical.functions]
    set_bij_lemmas.A [var, in mathcomp.classical.functions]
    set_bij_lemmas.aT [var, in mathcomp.classical.functions]
    set_bij_lemmas.aT [var, in mathcomp.classical.functions]
    set_bij_lemmas.aT [var, in mathcomp.classical.functions]
    set_bij_lemmas.B [var, in mathcomp.classical.functions]
    set_bij_lemmas.f [var, in mathcomp.classical.functions]
    set_bij_lemmas.fbij [var, in mathcomp.classical.functions]
    set_bij_lemmas.rT [var, in mathcomp.classical.functions]
    set_bij_lemmas.rT [var, in mathcomp.classical.functions]
    set_bij_lemmas.rT [var, in mathcomp.classical.functions]
    set_bij_sub [prf, in mathcomp.classical.functions]
    set_bij_surj [prf, in mathcomp.classical.functions]
    set_bool [prf, in mathcomp.classical.classical_sets]
    set_compose_diag [prf, in mathcomp.classical.classical_sets]
    set_compose_subset [prf, in mathcomp.classical.classical_sets]
    set_cons1 [prf, in mathcomp.classical.classical_sets]
    set_display [prf, in mathcomp.classical.classical_sets]
    set_eq_le [prf, in mathcomp.classical.classical_sets]
    set_ereal.E [var, in mathcomp.reals.real_interval]
    set_ereal.f [var, in mathcomp.reals.real_interval]
    set_ereal.g [var, in mathcomp.reals.real_interval]
    set_ereal.R [var, in mathcomp.reals.real_interval]
    set_ereal.T [var, in mathcomp.reals.real_interval]
    set_false [prf, in mathcomp.classical.classical_sets]
    set_fset0 [prf, in mathcomp.classical.classical_sets]
    set_fset1 [prf, in mathcomp.classical.classical_sets]
    set_fset_eq0 [prf, in mathcomp.classical.classical_sets]
    set_fsetD [prf, in mathcomp.classical.classical_sets]
    set_fsetD1 [prf, in mathcomp.classical.classical_sets]
    set_fsetI [prf, in mathcomp.classical.classical_sets]
    set_fsetIr [prf, in mathcomp.classical.classical_sets]
    set_fsetK [prf, in mathcomp.classical.cardinality]
    set_fsetU [prf, in mathcomp.classical.classical_sets]
    set_fsetU1 [prf, in mathcomp.classical.classical_sets]
    set_fun [def, in mathcomp.classical.functions]
    set_fun_image [prf, in mathcomp.classical.functions]
    set_imfset [prf, in mathcomp.classical.classical_sets]
    set_inj [def, in mathcomp.classical.functions]
    set_interval [file, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_Bij [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_Fun [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_Inject [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_InjFun [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_Inversible [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_InvFun [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_OInversible [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_OInvFun [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_SplitBij [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_SplitInj [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_SplitInjFun [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_SplitSurj [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_SplitSurjFun [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_Surject [def, in mathcomp.classical.set_interval]
    set_interval_ndline_path__canonical__functions_SurjFun [def, in mathcomp.classical.set_interval]
    set_itv1 [prf, in mathcomp.classical.set_interval]
    set_itv_bnd_ninfty [prf, in mathcomp.classical.set_interval]
    set_itv_c_infty [prf, in mathcomp.classical.set_interval]
    set_itv_ge [prf, in mathcomp.classical.set_interval]
    set_itv_infty_c [prf, in mathcomp.classical.set_interval]
    set_itv_infty_infty [prf, in mathcomp.classical.set_interval]
    set_itv_infty_o [prf, in mathcomp.classical.set_interval]
    set_itv_infty_set0 [def, in mathcomp.classical.set_interval]
    set_itv_latticeType.d [var, in mathcomp.classical.set_interval]
    set_itv_latticeType.T [var, in mathcomp.classical.set_interval]
    set_itv_numFieldType.R [var, in mathcomp.classical.set_interval]
    set_itv_o_infty [prf, in mathcomp.classical.set_interval]
    set_itv_orderType.d [var, in mathcomp.classical.set_interval]
    set_itv_orderType.T [var, in mathcomp.classical.set_interval]
    set_itv_pinfty_bnd [prf, in mathcomp.classical.set_interval]
    set_itv_porderType.d [var, in mathcomp.classical.set_interval]
    set_itv_porderType.d [var, in mathcomp.classical.set_interval]
    set_itv_porderType.T [var, in mathcomp.classical.set_interval]
    set_itv_porderType.T [var, in mathcomp.classical.set_interval]
    set_itv_realType.R [var, in mathcomp.reals.real_interval]
    set_itv_realType.R [var, in mathcomp.analysis.normedtype]
    set_itv_setT [prf, in mathcomp.analysis.normedtype]
    set_itv_splitD [prf, in mathcomp.classical.set_interval]
    set_itv_splitI [prf, in mathcomp.classical.set_interval]
    set_itvcc [prf, in mathcomp.classical.set_interval]
    set_itvco [prf, in mathcomp.classical.set_interval]
    set_itvco0 [prf, in mathcomp.classical.set_interval]
    set_itvE [def, in mathcomp.classical.set_interval]
    set_itvI [prf, in mathcomp.classical.set_interval]
    set_itvK [prf, in mathcomp.analysis.normedtype]
    set_itvoc [prf, in mathcomp.classical.set_interval]
    set_itvoc0 [prf, in mathcomp.classical.set_interval]
    set_itvoo [prf, in mathcomp.classical.set_interval]
    set_itvoo0 [prf, in mathcomp.classical.set_interval]
    set_itvP [prf, in mathcomp.classical.set_interval]
    set_itvxx [prf, in mathcomp.classical.set_interval]
    set_lte_bigcup [prf, in mathcomp.reals.real_interval]
    set_mem [prf, in mathcomp.classical.classical_sets]
    set_mem_set [prf, in mathcomp.classical.classical_sets]
    set_memK [prf, in mathcomp.classical.classical_sets]
    set_nbhs [def, in mathcomp.analysis.separation_axioms]
    set_nbhs.A [var, in mathcomp.analysis.separation_axioms]
    set_nbhs.T [var, in mathcomp.analysis.separation_axioms]
    set_nbhs_filter [inst, in mathcomp.analysis.separation_axioms]
    set_nbhs_pfilter [inst, in mathcomp.analysis.separation_axioms]
    set_nbhsP [prf, in mathcomp.analysis.separation_axioms]
    set_neq_lt [prf, in mathcomp.classical.classical_sets]
    set_nil [prf, in mathcomp.classical.classical_sets]
    set_of_fset_in_a_set.T [var, in mathcomp.analysis.esum]
    set_orb [prf, in mathcomp.classical.classical_sets]
    set_predC [prf, in mathcomp.classical.classical_sets]
    set_predType [def, in mathcomp.classical.classical_sets]
    set_prod_invK [prf, in mathcomp.classical.classical_sets]
    set_separations.T [var, in mathcomp.analysis.separation_axioms]
    set_seq_eq0 [prf, in mathcomp.classical.classical_sets]
    set_surj [def, in mathcomp.classical.functions]
    set_system [def, in mathcomp.classical.filter]
    set_true [prf, in mathcomp.classical.classical_sets]
    set_type [def, in mathcomp.classical.classical_sets]
    set_unit [prf, in mathcomp.classical.classical_sets]
    set_val [def, in mathcomp.classical.functions]
    set_val.A [var, in mathcomp.classical.functions]
    set_val.T [var, in mathcomp.classical.functions]
    set_valE [prf, in mathcomp.classical.functions]
    set_valP [prf, in mathcomp.classical.classical_sets]
    setC [def, in mathcomp.classical.classical_sets]
    setC0 [prf, in mathcomp.classical.classical_sets]
    setC_bigcap [prf, in mathcomp.classical.classical_sets]
    setC_bigcup [prf, in mathcomp.classical.classical_sets]
    setC_bigsetI [prf, in mathcomp.classical.classical_sets]
    setC_bigsetU [prf, in mathcomp.classical.classical_sets]
    setC_closed [def, in mathcomp.analysis.measure]
    setC_I [prf, in mathcomp.classical.classical_sets]
    setC_inj [def, in mathcomp.classical.classical_sets]
    setCD [prf, in mathcomp.classical.classical_sets]
    setCI [prf, in mathcomp.classical.classical_sets]
    setCitv [prf, in mathcomp.classical.set_interval]
    setCitvl [prf, in mathcomp.classical.set_interval]
    setCitvr [prf, in mathcomp.classical.set_interval]
    setCK [prf, in mathcomp.classical.classical_sets]
    setCS [prf, in mathcomp.classical.classical_sets]
    setCT [prf, in mathcomp.classical.classical_sets]
    setCU [prf, in mathcomp.classical.classical_sets]
    setCU_Efin [prf, in mathcomp.analysis.lebesgue_measure]
    setCYT [prf, in mathcomp.classical.classical_sets]
    setD [def, in mathcomp.classical.classical_sets]
    setD0 [prf, in mathcomp.classical.classical_sets]
    setD1K [prf, in mathcomp.classical.classical_sets]
    setD_bigcup [prf, in mathcomp.classical.classical_sets]
    setD_bigcupl [prf, in mathcomp.classical.classical_sets]
    setD_closed [abbrev, in mathcomp.analysis.measure]
    setD_eq0 [prf, in mathcomp.classical.classical_sets]
    setDD [prf, in mathcomp.classical.classical_sets]
    setDDl [prf, in mathcomp.classical.classical_sets]
    setDDr [prf, in mathcomp.classical.classical_sets]
    setDE [prf, in mathcomp.classical.classical_sets]
    setDI_closed [def, in mathcomp.analysis.measure]
    setDI_semi_setD_closed [prf, in mathcomp.analysis.measure]
    setDidl [prf, in mathcomp.classical.classical_sets]
    setDidPl [prf, in mathcomp.classical.classical_sets]
    setDIK [prf, in mathcomp.classical.classical_sets]
    setDIr [prf, in mathcomp.classical.classical_sets]
    setDitv1l [prf, in mathcomp.classical.set_interval]
    setDitv1r [prf, in mathcomp.classical.set_interval]
    setDKI [prf, in mathcomp.classical.classical_sets]
    setDKU [prf, in mathcomp.classical.classical_sets]
    setDS [prf, in mathcomp.classical.classical_sets]
    setDSS [prf, in mathcomp.classical.classical_sets]
    setDT [prf, in mathcomp.classical.classical_sets]
    setDU [prf, in mathcomp.classical.classical_sets]
    setDUD [prf, in mathcomp.classical.classical_sets]
    setDUK [prf, in mathcomp.classical.classical_sets]
    setDUl [prf, in mathcomp.classical.classical_sets]
    setDUr [prf, in mathcomp.classical.classical_sets]
    setDv [prf, in mathcomp.classical.classical_sets]
    seteqfun [def, in mathcomp.classical.functions]
    seteqfun.A [var, in mathcomp.classical.functions]
    seteqfun.AB [var, in mathcomp.classical.functions]
    seteqfun.B [var, in mathcomp.classical.functions]
    seteqfun.T [var, in mathcomp.classical.functions]
    seteqfun_can2_subproof [prf, in mathcomp.classical.functions]
    seteqP [prf, in mathcomp.classical.classical_sets]
    setF_eq0 [prf, in mathcomp.classical.classical_sets]
    SetFset.T [var, in mathcomp.classical.classical_sets]
    setI [def, in mathcomp.classical.classical_sets]
    setI0 [prf, in mathcomp.classical.classical_sets]
    setI1 [prf, in mathcomp.classical.classical_sets]
    setI_bigcupl [prf, in mathcomp.classical.classical_sets]
    setI_bigcupr [prf, in mathcomp.classical.classical_sets]
    setI_closed [def, in mathcomp.analysis.measure]
    setI_closed_g_dynkin_g_sigma_algebra [prf, in mathcomp.analysis.measure]
    setI_closed_gdynkin_salgebra [abbrev, in mathcomp.analysis.measure]
    setI_g_sigma_ring [prf, in mathcomp.analysis.measure]
    setI_II [prf, in mathcomp.classical.classical_sets]
    setIA [prf, in mathcomp.classical.classical_sets]
    setIAC [prf, in mathcomp.classical.classical_sets]
    setIACA [prf, in mathcomp.classical.classical_sets]
    setIC [prf, in mathcomp.classical.classical_sets]
    setICA [prf, in mathcomp.classical.classical_sets]
    setICK [prf, in mathcomp.classical.classical_sets]
    setICl [prf, in mathcomp.classical.classical_sets]
    setICr [prf, in mathcomp.classical.classical_sets]
    setIDA [prf, in mathcomp.classical.classical_sets]
    setIDAC [prf, in mathcomp.classical.classical_sets]
    setIid [prf, in mathcomp.classical.classical_sets]
    setIidl [prf, in mathcomp.classical.classical_sets]
    setIidPl [prf, in mathcomp.classical.classical_sets]
    setIidPr [prf, in mathcomp.classical.classical_sets]
    setIidr [prf, in mathcomp.classical.classical_sets]
    setIIl [prf, in mathcomp.classical.classical_sets]
    setIIr [prf, in mathcomp.classical.classical_sets]
    setIK [prf, in mathcomp.classical.classical_sets]
    setIKC [prf, in mathcomp.classical.classical_sets]
    setIS [prf, in mathcomp.classical.classical_sets]
    setISS [prf, in mathcomp.classical.classical_sets]
    setIT [prf, in mathcomp.classical.classical_sets]
    setitv0 [prf, in mathcomp.classical.set_interval]
    setIUl [prf, in mathcomp.classical.classical_sets]
    setIUr [prf, in mathcomp.classical.classical_sets]
    setIv [abbrev, in mathcomp.classical.classical_sets]
    setIYl [prf, in mathcomp.classical.classical_sets]
    setIYr [prf, in mathcomp.classical.classical_sets]
    setKI [prf, in mathcomp.classical.classical_sets]
    setKU [prf, in mathcomp.classical.classical_sets]
    setM [abbrev, in mathcomp.classical.classical_sets]
    setM0 [abbrev, in mathcomp.classical.classical_sets]
    setM_bigcupl [abbrev, in mathcomp.classical.classical_sets]
    setM_bigcupr [abbrev, in mathcomp.classical.classical_sets]
    setMI [abbrev, in mathcomp.classical.classical_sets]
    setML [abbrev, in mathcomp.classical.classical_sets]
    SetMonoids.T [var, in mathcomp.classical.classical_sets]
    setMR [abbrev, in mathcomp.classical.classical_sets]
    setMT [abbrev, in mathcomp.classical.classical_sets]
    setMTT [abbrev, in mathcomp.classical.classical_sets]
    setNK [prf, in mathcomp.classical.set_interval]
    SetOrder [mod, in mathcomp.classical.classical_sets]
    SetOrder.Exports [mod, in mathcomp.classical.classical_sets]
    SetOrder.Exports.botEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.complEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.exports.T [var, in mathcomp.classical.classical_sets]
    SetOrder.Exports.joinEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.meetEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.properEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.properPset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.subEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.subsetEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.subsetPset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.topEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal [mod, in mathcomp.classical.classical_sets]
    SetOrder.Internal.choice_Choice__to__choice_hasChoice [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.choice_Choice__to__eqtype_hasDecEq [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__choice_Choice [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__eqtype_Equality [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__Order_BDistrLattice [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__Order_BLattice [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__Order_BPOrder [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__Order_CBDistrLattice [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__Order_CTBDistrLattice [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__Order_DistrLattice [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__Order_Lattice [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__Order_POrder [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__Order_TBDistrLattice [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__Order_TBLattice [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__Order_TBPOrder [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__Order_TLattice [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.classical_sets_set__canonical__Order_TPOrder [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.Exports [mod, in mathcomp.classical.classical_sets]
    SetOrder.Internal.HB_unnamed_factory_106 [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.HB_unnamed_factory_108 [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.HB_unnamed_factory_110 [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.HB_unnamed_factory_112 [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.HB_unnamed_factory_94 [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.HB_unnamed_factory_99 [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.HB_unnamed_mixin_103 [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.HB_unnamed_mixin_104 [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.HB_unnamed_mixin_105 [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.HB_unnamed_mixin_97 [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.HB_unnamed_mixin_98 [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.joinIB [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.joinKI [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.le_def [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.lt_def [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.meetKU [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.Order_isMeetJoinDistrLattice__to__Order_isPOrder [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.Order_isMeetJoinDistrLattice__to__Order_Lattice_Meet_isDistrLattice [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.Order_isMeetJoinDistrLattice__to__Order_POrder_isLattice [def, in mathcomp.classical.classical_sets]
    SetOrder.Internal.SetOrder.T [var, in mathcomp.classical.classical_sets]
    SetOrder.Internal.SetOrder_setTsub [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.SetOrder_sub0set [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.subKI [prf, in mathcomp.classical.classical_sets]
    SetRing [mod, in mathcomp.analysis.measure]
    setring [def, in mathcomp.analysis.measure]
    SetRing.all_decomp_neq0 [prf, in mathcomp.analysis.measure]
    SetRing.classical_sets_Pointed__to__choice_hasChoice [def, in mathcomp.analysis.measure]
    SetRing.classical_sets_Pointed__to__classical_sets_isPointed [def, in mathcomp.analysis.measure]
    SetRing.classical_sets_Pointed__to__eqtype_hasDecEq [def, in mathcomp.analysis.measure]
    SetRing.cover_decomp [prf, in mathcomp.analysis.measure]
    SetRing.decomp [def, in mathcomp.analysis.measure]
    SetRing.decomp_finite_set [prf, in mathcomp.analysis.measure]
    SetRing.decomp_measurable [prf, in mathcomp.analysis.measure]
    SetRing.decomp_neq0 [prf, in mathcomp.analysis.measure]
    SetRing.decomp_set0 [prf, in mathcomp.analysis.measure]
    SetRing.decomp_sub [prf, in mathcomp.analysis.measure]
    SetRing.decomp_triv [prf, in mathcomp.analysis.measure]
    SetRing.decompN0 [prf, in mathcomp.analysis.measure]
    SetRing.display [def, in mathcomp.analysis.measure]
    SetRing.Exports [mod, in mathcomp.analysis.measure]
    SetRing.HB_unnamed_factory_167 [def, in mathcomp.analysis.measure]
    SetRing.HB_unnamed_factory_174 [def, in mathcomp.analysis.measure]
    SetRing.HB_unnamed_factory_179 [def, in mathcomp.analysis.measure]
    SetRing.HB_unnamed_mixin_171 [def, in mathcomp.analysis.measure]
    SetRing.HB_unnamed_mixin_172 [def, in mathcomp.analysis.measure]
    SetRing.HB_unnamed_mixin_173 [def, in mathcomp.analysis.measure]
    SetRing.HB_unnamed_mixin_177 [def, in mathcomp.analysis.measure]
    SetRing.HB_unnamed_mixin_178 [def, in mathcomp.analysis.measure]
    SetRing.measurable_fin_trivIset [def, in mathcomp.analysis.measure]
    SetRing.measurable_subring [prf, in mathcomp.analysis.measure]
    SetRing.measure [def, in mathcomp.analysis.measure]
    SetRing.measure_isRingOfSets__to__measure_isSemiRingOfSets [def, in mathcomp.analysis.measure]
    SetRing.measure_isRingOfSets__to__measure_SemiRingOfSets_isRingOfSets [def, in mathcomp.analysis.measure]
    SetRing.ring_finite_set [prf, in mathcomp.analysis.measure]
    SetRing.ring_measurableE [prf, in mathcomp.analysis.measure]
    SetRing.Rmu [abbrev, in mathcomp.analysis.measure]
    SetRing.Rmu_additive [prf, in mathcomp.analysis.measure]
    SetRing.Rmu_fin_bigcup [prf, in mathcomp.analysis.measure]
    SetRing.Rmu_ge0 [prf, in mathcomp.analysis.measure]
    SetRing.RmuE [prf, in mathcomp.analysis.measure]
    SetRing.rT [abbrev, in mathcomp.analysis.measure]
    .-ring [not, in mathcomp.analysis.measure] (no scope)
    .-ring.-measurable [not, in mathcomp.analysis.measure] (no scope)
    SetRing.SetRing.content.mu [var, in mathcomp.analysis.measure]
    SetRing.SetRing.content.R [var, in mathcomp.analysis.measure]
    SetRing.SetRing.content.Rmu0 [var, in mathcomp.analysis.measure]
    SetRing.SetRing.d [var, in mathcomp.analysis.measure]
    SetRing.SetRing.T [var, in mathcomp.analysis.measure]
    SetRing.SetRing_measure__canonical__measure_Content [def, in mathcomp.analysis.measure]
    SetRing.SetRing_type__canonical__choice_Choice [def, in mathcomp.analysis.measure]
    SetRing.SetRing_type__canonical__classical_sets_Pointed [def, in mathcomp.analysis.measure]
    SetRing.SetRing_type__canonical__eqtype_Equality [def, in mathcomp.analysis.measure]
    SetRing.SetRing_type__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
    SetRing.SetRing_type__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
    SetRing.type [def, in mathcomp.analysis.measure]
    setring0 [prf, in mathcomp.analysis.measure]
    setring_fin_bigcup [prf, in mathcomp.analysis.measure]
    setring_id [prf, in mathcomp.analysis.measure]
    SetRing_measure__canonical__measure_Measure [def, in mathcomp.analysis.measure]
    setring_monotone_sigma_ring [prf, in mathcomp.analysis.measure]
    setringDI [prf, in mathcomp.analysis.measure]
    setringU [prf, in mathcomp.analysis.measure]
    setSD [prf, in mathcomp.classical.classical_sets]
    setSD_closed [def, in mathcomp.analysis.measure]
    setSI [prf, in mathcomp.classical.classical_sets]
    setSM [abbrev, in mathcomp.classical.classical_sets]
    setSU [prf, in mathcomp.classical.classical_sets]
    setSX [prf, in mathcomp.classical.classical_sets]
    setT [def, in mathcomp.classical.classical_sets]
    setT0 [prf, in mathcomp.classical.classical_sets]
    setT_bool [prf, in mathcomp.classical.classical_sets]
    setT_unit [prf, in mathcomp.classical.classical_sets]
    setTbij [def, in mathcomp.classical.functions]
    setTD [prf, in mathcomp.classical.classical_sets]
    setTI [prf, in mathcomp.classical.classical_sets]
    setTM [abbrev, in mathcomp.classical.classical_sets]
    setTP [abbrev, in mathcomp.classical.classical_sets]
    setTPn [prf, in mathcomp.classical.classical_sets]
    setTT_bijective [prf, in mathcomp.classical.functions]
    setTU [prf, in mathcomp.classical.classical_sets]
    setTX [prf, in mathcomp.classical.classical_sets]
    setTYC [prf, in mathcomp.classical.classical_sets]
    setU [def, in mathcomp.classical.classical_sets]
    setU0 [prf, in mathcomp.classical.classical_sets]
    setU1itv [prf, in mathcomp.classical.set_interval]
    setU_bigcapl [prf, in mathcomp.classical.classical_sets]
    setU_bigcapr [prf, in mathcomp.classical.classical_sets]
    setU_closed [def, in mathcomp.analysis.measure]
    setU_eq0 [prf, in mathcomp.classical.classical_sets]
    setU_id2r [prf, in mathcomp.classical.classical_sets]
    setU_II [prf, in mathcomp.classical.classical_sets]
    setU_seqD [prf, in mathcomp.analysis.sequences]
    setUA [prf, in mathcomp.classical.classical_sets]
    setUAC [prf, in mathcomp.classical.classical_sets]
    setUACA [prf, in mathcomp.classical.classical_sets]
    setUC [prf, in mathcomp.classical.classical_sets]
    setUCA [prf, in mathcomp.classical.classical_sets]
    setUCK [prf, in mathcomp.classical.classical_sets]
    setUCl [prf, in mathcomp.classical.classical_sets]
    setUCr [prf, in mathcomp.classical.classical_sets]
    setUDK [prf, in mathcomp.classical.classical_sets]
    setUid [prf, in mathcomp.classical.classical_sets]
    setUIDK [prf, in mathcomp.classical.classical_sets]
    setUidl [prf, in mathcomp.classical.classical_sets]
    setUidPl [prf, in mathcomp.classical.classical_sets]
    setUidPr [prf, in mathcomp.classical.classical_sets]
    setUidr [prf, in mathcomp.classical.classical_sets]
    setUIl [prf, in mathcomp.classical.classical_sets]
    setUIr [prf, in mathcomp.classical.classical_sets]
    setUitv1 [prf, in mathcomp.classical.set_interval]
    setUK [prf, in mathcomp.classical.classical_sets]
    setUKC [prf, in mathcomp.classical.classical_sets]
    setUKD [prf, in mathcomp.classical.classical_sets]
    setUS [prf, in mathcomp.classical.classical_sets]
    setUSS [prf, in mathcomp.classical.classical_sets]
    setUT [prf, in mathcomp.classical.classical_sets]
    setUUl [prf, in mathcomp.classical.classical_sets]
    setUUr [prf, in mathcomp.classical.classical_sets]
    setUv [prf, in mathcomp.classical.classical_sets]
    setvI [abbrev, in mathcomp.classical.classical_sets]
    setvU [prf, in mathcomp.classical.classical_sets]
    setX [def, in mathcomp.classical.classical_sets]
    setX0 [prf, in mathcomp.classical.classical_sets]
    setX_bigcupl [prf, in mathcomp.classical.classical_sets]
    setX_bigcupr [prf, in mathcomp.classical.classical_sets]
    setX_of_sigT [def, in mathcomp.analysis.topology_theory.subtype_topology]
    setX_of_sigT_continuous [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    setX_of_sigTK [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    setXI [prf, in mathcomp.classical.classical_sets]
    setXL [def, in mathcomp.classical.classical_sets]
    setXR [def, in mathcomp.classical.classical_sets]
    setXT [prf, in mathcomp.classical.classical_sets]
    setXTT [prf, in mathcomp.classical.classical_sets]
    setY [def, in mathcomp.classical.classical_sets]
    setY0 [prf, in mathcomp.classical.classical_sets]
    setY_closed [def, in mathcomp.analysis.measure]
    setY_def [prf, in mathcomp.classical.classical_sets]
    setYA [prf, in mathcomp.classical.classical_sets]
    setYC [prf, in mathcomp.classical.classical_sets]
    setYCT [prf, in mathcomp.classical.classical_sets]
    setYD [prf, in mathcomp.classical.classical_sets]
    setYE [prf, in mathcomp.classical.classical_sets]
    setYI [prf, in mathcomp.classical.classical_sets]
    setYK [prf, in mathcomp.classical.classical_sets]
    setYTC [prf, in mathcomp.classical.classical_sets]
    setYU [prf, in mathcomp.classical.classical_sets]
    sfinite.d [var, in mathcomp.analysis.kernel]
    sfinite.d' [var, in mathcomp.analysis.kernel]
    sfinite.hb_instance_12.n [var, in mathcomp.analysis.kernel]
    sfinite.hb_instance_15.n [var, in mathcomp.analysis.kernel]
    sfinite.k [var, in mathcomp.analysis.kernel]
    sfinite.ms [var, in mathcomp.analysis.kernel]
    sfinite.R [var, in mathcomp.analysis.kernel]
    sfinite.s [var, in mathcomp.analysis.kernel]
    sfinite.s_uub [var, in mathcomp.analysis.kernel]
    sfinite.X [var, in mathcomp.analysis.kernel]
    sfinite.Y [var, in mathcomp.analysis.kernel]
    sfinite_Fubini [prf, in mathcomp.analysis.lebesgue_integral]
    sfinite_fubini.d [var, in mathcomp.analysis.lebesgue_integral]
    sfinite_fubini.d' [var, in mathcomp.analysis.lebesgue_integral]
    sfinite_fubini.f [var, in mathcomp.analysis.lebesgue_integral]
    sfinite_fubini.f0 [var, in mathcomp.analysis.lebesgue_integral]
    sfinite_fubini.m1 [var, in mathcomp.analysis.lebesgue_integral]
    sfinite_fubini.m2 [var, in mathcomp.analysis.lebesgue_integral]
    sfinite_fubini.mf [var, in mathcomp.analysis.lebesgue_integral]
    sfinite_fubini.R [var, in mathcomp.analysis.lebesgue_integral]
    sfinite_fubini.X [var, in mathcomp.analysis.lebesgue_integral]
    sfinite_fubini.Y [var, in mathcomp.analysis.lebesgue_integral]
    sfinite_kernel [prf, in mathcomp.analysis.kernel]
    sfinite_kernel_measure [prf, in mathcomp.analysis.kernel]
    sfinite_kernel_subdef [def, in mathcomp.analysis.kernel]
    sfinite_measure [def, in mathcomp.analysis.measure]
    sfinite_measure.d [var, in mathcomp.analysis.measure]
    sfinite_measure.hb_instance_232.n [var, in mathcomp.analysis.measure]
    sfinite_measure.hb_instance_240.n [var, in mathcomp.analysis.measure]
    sfinite_measure.mu [var, in mathcomp.analysis.measure]
    sfinite_measure.R [var, in mathcomp.analysis.measure]
    sfinite_measure.s [var, in mathcomp.analysis.measure]
    sfinite_measure.s0 [var, in mathcomp.analysis.measure]
    sfinite_measure.s_fin [var, in mathcomp.analysis.measure]
    sfinite_measure.s_ge0 [var, in mathcomp.analysis.measure]
    sfinite_measure.s_semi_sigma_additive [var, in mathcomp.analysis.measure]
    sfinite_measure.T [var, in mathcomp.analysis.measure]
    sfinite_measure_seq [def, in mathcomp.analysis.measure]
    sfinite_measure_seqP [prf, in mathcomp.analysis.measure]
    sfinite_measure_sigma_finite [prf, in mathcomp.analysis.measure]
    sfinite_measure_subdef [abbrev, in mathcomp.analysis.measure]
    sfinite_mzero [prf, in mathcomp.analysis.measure]
    SFiniteKernel [mod, in mathcomp.analysis.kernel]
    SFiniteKernel.axioms_ [rec, in mathcomp.analysis.kernel]
    SFiniteKernel.class [proj, in mathcomp.analysis.kernel]
    SFiniteKernel.Exports [mod, in mathcomp.analysis.kernel]
    SFiniteKernel.Exports.kernel_SFiniteKernel__to__kernel_Kernel [def, in mathcomp.analysis.kernel]
    SFiniteKernel.Exports.kernel_SFiniteKernel_class__to__kernel_Kernel_class [def, in mathcomp.analysis.kernel]
    SFiniteKernel.kernel_isKernel_mixin [proj, in mathcomp.analysis.kernel]
    SFiniteKernel.kernel_Kernel_isSFinite_subdef_mixin [proj, in mathcomp.analysis.kernel]
    SFiniteKernel.pack_ [def, in mathcomp.analysis.kernel]
    SFiniteKernel.phant_clone [def, in mathcomp.analysis.kernel]
    SFiniteKernel.phant_on_ [def, in mathcomp.analysis.kernel]
    SFiniteKernel.sort [proj, in mathcomp.analysis.kernel]
    SFiniteKernel.type [rec, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite [mod, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite.axioms_ [rec, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite.Exports [mod, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite.identity_builder [def, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite.measure_uub [proj, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite.phant_axioms [def, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite.phant_Build [def, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite.SFiniteKernel_isFinite.d [var, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite.SFiniteKernel_isFinite.d' [var, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite.SFiniteKernel_isFinite.k [var, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite.SFiniteKernel_isFinite.R [var, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite.SFiniteKernel_isFinite.X [var, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite.SFiniteKernel_isFinite.Y [var, in mathcomp.analysis.kernel]
    SFiniteKernelElpiOperations [mod, in mathcomp.analysis.kernel]
    SFiniteMeasure [mod, in mathcomp.analysis.measure]
    SFiniteMeasure.axioms_ [rec, in mathcomp.analysis.measure]
    SFiniteMeasure.class [proj, in mathcomp.analysis.measure]
    SFiniteMeasure.Exports [mod, in mathcomp.analysis.measure]
    SFiniteMeasure.Exports.measure_SFiniteMeasure__to__measure_Content [def, in mathcomp.analysis.measure]
    SFiniteMeasure.Exports.measure_SFiniteMeasure__to__measure_Measure [def, in mathcomp.analysis.measure]
    SFiniteMeasure.Exports.measure_SFiniteMeasure_class__to__measure_Content_class [def, in mathcomp.analysis.measure]
    SFiniteMeasure.Exports.measure_SFiniteMeasure_class__to__measure_Measure_class [def, in mathcomp.analysis.measure]
    SFiniteMeasure.measure_Content_isMeasure_mixin [proj, in mathcomp.analysis.measure]
    SFiniteMeasure.measure_isContent_mixin [proj, in mathcomp.analysis.measure]
    SFiniteMeasure.measure_isSFinite_mixin [proj, in mathcomp.analysis.measure]
    SFiniteMeasure.pack_ [def, in mathcomp.analysis.measure]
    SFiniteMeasure.phant_clone [def, in mathcomp.analysis.measure]
    SFiniteMeasure.phant_on_ [def, in mathcomp.analysis.measure]
    SFiniteMeasure.sort [proj, in mathcomp.analysis.measure]
    SFiniteMeasure.type [rec, in mathcomp.analysis.measure]
    SFiniteMeasureElpiOperations [mod, in mathcomp.analysis.measure]
    sfkadd.d [var, in mathcomp.analysis.kernel]
    sfkadd.d' [var, in mathcomp.analysis.kernel]
    sfkadd.hb_instance_87.t [var, in mathcomp.analysis.kernel]
    sfkadd.k1 [var, in mathcomp.analysis.kernel]
    sfkadd.k2 [var, in mathcomp.analysis.kernel]
    sfkadd.R [var, in mathcomp.analysis.kernel]
    sfkadd.sfinite_kadd [var, in mathcomp.analysis.kernel]
    sfkadd.X [var, in mathcomp.analysis.kernel]
    sfkadd.Y [var, in mathcomp.analysis.kernel]
    sfkseries.d [var, in mathcomp.analysis.kernel]
    sfkseries.d' [var, in mathcomp.analysis.kernel]
    sfkseries.k [var, in mathcomp.analysis.kernel]
    sfkseries.R [var, in mathcomp.analysis.kernel]
    sfkseries.sfinite_kseries [var, in mathcomp.analysis.kernel]
    sfkseries.X [var, in mathcomp.analysis.kernel]
    sfkseries.Y [var, in mathcomp.analysis.kernel]
    sfun [abbrev, in mathcomp.analysis.lebesgue_integral]
    sfun [def, in mathcomp.analysis.lebesgue_integral]
    sfun.aT [var, in mathcomp.analysis.lebesgue_integral]
    sfun.d [var, in mathcomp.analysis.lebesgue_integral]
    sfun.hb_instance_88.x [var, in mathcomp.analysis.lebesgue_integral]
    sfun.rT [var, in mathcomp.analysis.lebesgue_integral]
    sfun.Sub.f [var, in mathcomp.analysis.lebesgue_integral]
    sfun.Sub.fP [var, in mathcomp.analysis.lebesgue_integral]
    sfun0 [prf, in mathcomp.analysis.lebesgue_integral]
    sfun1 [prf, in mathcomp.analysis.lebesgue_integral]
    sfun_fubini_tonelli [prf, in mathcomp.analysis.lebesgue_integral]
    sfun_fubini_tonelli1 [prf, in mathcomp.analysis.lebesgue_integral]
    sfun_fubini_tonelli2 [prf, in mathcomp.analysis.lebesgue_integral]
    sfun_fubini_tonelli_FE [prf, in mathcomp.analysis.lebesgue_integral]
    sfun_fubini_tonelli_GE [prf, in mathcomp.analysis.lebesgue_integral]
    sfun_key [def, in mathcomp.analysis.lebesgue_integral]
    sfun_keyed [def, in mathcomp.analysis.lebesgue_integral]
    sfun_measurable_fun_fubini_tonelli_F [prf, in mathcomp.analysis.lebesgue_integral]
    sfun_measurable_fun_fubini_tonelli_G [prf, in mathcomp.analysis.lebesgue_integral]
    sfun_pred.aT [var, in mathcomp.analysis.lebesgue_integral]
    sfun_pred.d [var, in mathcomp.analysis.lebesgue_integral]
    sfun_pred.rT [var, in mathcomp.analysis.lebesgue_integral]
    sfun_prod [prf, in mathcomp.analysis.lebesgue_integral]
    sfun_rect [prf, in mathcomp.analysis.lebesgue_integral]
    sfun_Sub [def, in mathcomp.analysis.lebesgue_integral]
    sfun_Sub1_subproof [def, in mathcomp.analysis.lebesgue_integral]
    sfun_Sub2_subproof [def, in mathcomp.analysis.lebesgue_integral]
    sfun_subring_closed [prf, in mathcomp.analysis.lebesgue_integral]
    sfun_sum [prf, in mathcomp.analysis.lebesgue_integral]
    sfun_valP [prf, in mathcomp.analysis.lebesgue_integral]
    sfunB [prf, in mathcomp.analysis.lebesgue_integral]
    sfunD [prf, in mathcomp.analysis.lebesgue_integral]
    sfuneqP [prf, in mathcomp.analysis.lebesgue_integral]
    sfunM [prf, in mathcomp.analysis.lebesgue_integral]
    sfunN [prf, in mathcomp.analysis.lebesgue_integral]
    sfunX [prf, in mathcomp.analysis.lebesgue_integral]
    shift [def, in mathcomp.analysis.normedtype]
    Shift.R [var, in mathcomp.analysis.normedtype]
    Shift.T [var, in mathcomp.analysis.normedtype]
    shift0 [prf, in mathcomp.analysis.normedtype]
    ShortFunSyntax [mod, in mathcomp.classical.functions]
    <<=> [not, in mathcomp.classical.functions] (in type_scope)
    <<~ [not, in mathcomp.classical.functions] (in type_scope)
    <<~> [not, in mathcomp.classical.functions] (in type_scope)
    <=> [not, in mathcomp.classical.functions] (in type_scope)
    <~ [not, in mathcomp.classical.functions] (in type_scope)
    <~> [not, in mathcomp.classical.functions] (in type_scope)
    ==>> [not, in mathcomp.classical.functions] (in type_scope)
    =>> [not, in mathcomp.classical.functions] (in type_scope)
    >=> [not, in mathcomp.classical.functions] (in type_scope)
    >>=> [not, in mathcomp.classical.functions] (in type_scope)
    >>~> [not, in mathcomp.classical.functions] (in type_scope)
    >~> [not, in mathcomp.classical.functions] (in type_scope)
    ~> [not, in mathcomp.classical.functions] (in type_scope)
    ~>> [not, in mathcomp.classical.functions] (in type_scope)
    ~~>> [not, in mathcomp.classical.functions] (in type_scope)
    showo [prf, in mathcomp.analysis.landau]
    sigL [def, in mathcomp.classical.functions]
    sigL2K [prf, in mathcomp.classical.functions]
    sigL_arrow [def, in mathcomp.analysis.function_spaces]
    sigL_bijP [prf, in mathcomp.classical.functions]
    sigL_funP [prf, in mathcomp.classical.functions]
    sigL_inj_subproof [prf, in mathcomp.classical.functions]
    sigL_injP [prf, in mathcomp.classical.functions]
    sigL_isfun [prf, in mathcomp.classical.functions]
    sigL_restrict [prf, in mathcomp.classical.functions]
    sigL_some_inv [prf, in mathcomp.classical.functions]
    sigL_surj_subproof [prf, in mathcomp.classical.functions]
    sigL_surjP [prf, in mathcomp.classical.functions]
    sigL_valL [prf, in mathcomp.classical.functions]
    sigL_valLfun [prf, in mathcomp.classical.functions]
    sigLE [prf, in mathcomp.classical.functions]
    sigLfun [def, in mathcomp.classical.functions]
    sigLK [prf, in mathcomp.classical.functions]
    sigLR [def, in mathcomp.classical.functions]
    sigLR_bijP [prf, in mathcomp.classical.functions]
    sigLR_injP [prf, in mathcomp.classical.functions]
    sigLR_surjP [prf, in mathcomp.classical.functions]
    sigLRfun_bijP [prf, in mathcomp.classical.functions]
    sigma_additive [def, in mathcomp.analysis.measure]
    sigma_additive_is_additive [prf, in mathcomp.analysis.measure]
    sigma_algebra [def, in mathcomp.analysis.measure]
    sigma_algebra0 [prf, in mathcomp.analysis.measure]
    sigma_algebra_bigcap [prf, in mathcomp.analysis.measure]
    sigma_algebra_bigcup [prf, in mathcomp.analysis.measure]
    sigma_algebra_dynkin [prf, in mathcomp.analysis.measure]
    sigma_algebra_id [prf, in mathcomp.analysis.measure]
    sigma_algebra_image_class [prf, in mathcomp.analysis.measure]
    sigma_algebra_measurable [prf, in mathcomp.analysis.measure]
    sigma_algebra_preimage_class [prf, in mathcomp.analysis.measure]
    sigma_algebra_preimage_classE [prf, in mathcomp.analysis.measure]
    sigma_algebra_strace [prf, in mathcomp.analysis.measure]
    sigma_algebraC [prf, in mathcomp.analysis.measure]
    sigma_algebraCD [prf, in mathcomp.analysis.measure]
    sigma_algebraP [prf, in mathcomp.analysis.measure]
    sigma_display [def, in mathcomp.analysis.measure]
    sigma_finite [def, in mathcomp.analysis.measure]
    sigma_finite_counting [prf, in mathcomp.analysis.measure]
    sigma_finite_lemma.A [var, in mathcomp.analysis.measure]
    sigma_finite_lemma.d [var, in mathcomp.analysis.measure]
    sigma_finite_lemma.mu [var, in mathcomp.analysis.measure]
    sigma_finite_lemma.R [var, in mathcomp.analysis.measure]
    sigma_finite_lemma.T [var, in mathcomp.analysis.measure]
    sigma_finite_mzero [prf, in mathcomp.analysis.measure]
    sigma_finiteP [prf, in mathcomp.analysis.measure]
    sigma_finiteT [def, in mathcomp.analysis.measure]
    sigma_ring [def, in mathcomp.analysis.measure]
    sigma_ring_lambda_system.d [var, in mathcomp.analysis.measure]
    sigma_ring_lambda_system.T [var, in mathcomp.analysis.measure]
    sigma_ring_monotone [prf, in mathcomp.analysis.measure]
    sigma_sub_additive [abbrev, in mathcomp.analysis.measure]
    sigma_subadditive [def, in mathcomp.analysis.measure]
    SigmaFiniteContent [mod, in mathcomp.analysis.measure]
    SigmaFiniteContent.axioms_ [rec, in mathcomp.analysis.measure]
    SigmaFiniteContent.class [proj, in mathcomp.analysis.measure]
    SigmaFiniteContent.Exports [mod, in mathcomp.analysis.measure]
    SigmaFiniteContent.Exports.measure_SigmaFiniteContent__to__measure_Content [def, in mathcomp.analysis.measure]
    SigmaFiniteContent.Exports.measure_SigmaFiniteContent_class__to__measure_Content_class [def, in mathcomp.analysis.measure]
    SigmaFiniteContent.measure_isContent_mixin [proj, in mathcomp.analysis.measure]
    SigmaFiniteContent.measure_isSigmaFinite_mixin [proj, in mathcomp.analysis.measure]
    SigmaFiniteContent.pack_ [def, in mathcomp.analysis.measure]
    SigmaFiniteContent.phant_clone [def, in mathcomp.analysis.measure]
    SigmaFiniteContent.phant_on_ [def, in mathcomp.analysis.measure]
    SigmaFiniteContent.sort [proj, in mathcomp.analysis.measure]
    SigmaFiniteContent.type [rec, in mathcomp.analysis.measure]
    SigmaFiniteContentElpiOperations [mod, in mathcomp.analysis.measure]
    SigmaFiniteMeasure [mod, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.axioms_ [rec, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.class [proj, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.Exports [mod, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.Exports.join_measure_SigmaFiniteMeasure_between_measure_Measure_and_measure_SigmaFiniteContent [def, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.Exports.join_measure_SigmaFiniteMeasure_between_measure_SFiniteMeasure_and_measure_SigmaFiniteContent [def, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.Exports.measure_SigmaFiniteMeasure__to__measure_Content [def, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.Exports.measure_SigmaFiniteMeasure__to__measure_Measure [def, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.Exports.measure_SigmaFiniteMeasure__to__measure_SFiniteMeasure [def, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.Exports.measure_SigmaFiniteMeasure__to__measure_SigmaFiniteContent [def, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.Exports.measure_SigmaFiniteMeasure_class__to__measure_Content_class [def, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.Exports.measure_SigmaFiniteMeasure_class__to__measure_Measure_class [def, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.Exports.measure_SigmaFiniteMeasure_class__to__measure_SFiniteMeasure_class [def, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.Exports.measure_SigmaFiniteMeasure_class__to__measure_SigmaFiniteContent_class [def, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.measure_Content_isMeasure_mixin [proj, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.measure_isContent_mixin [proj, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.measure_isSFinite_mixin [proj, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.measure_isSigmaFinite_mixin [proj, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.pack_ [def, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.phant_clone [def, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.phant_on_ [def, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.sort [proj, in mathcomp.analysis.measure]
    SigmaFiniteMeasure.type [rec, in mathcomp.analysis.measure]
    SigmaFiniteMeasureElpiOperations [mod, in mathcomp.analysis.measure]
    SigmaRing [mod, in mathcomp.analysis.measure]
    SigmaRing.axioms_ [rec, in mathcomp.analysis.measure]
    SigmaRing.choice_hasChoice_mixin [proj, in mathcomp.analysis.measure]
    SigmaRing.class [proj, in mathcomp.analysis.measure]
    SigmaRing.classical_sets_isPointed_mixin [proj, in mathcomp.analysis.measure]
    SigmaRing.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.measure]
    SigmaRing.Exports [mod, in mathcomp.analysis.measure]
    SigmaRing.Exports.measure_SigmaRing__to__choice_Choice [def, in mathcomp.analysis.measure]
    SigmaRing.Exports.measure_SigmaRing__to__classical_sets_Pointed [def, in mathcomp.analysis.measure]
    SigmaRing.Exports.measure_SigmaRing__to__eqtype_Equality [def, in mathcomp.analysis.measure]
    SigmaRing.Exports.measure_SigmaRing__to__measure_RingOfSets [def, in mathcomp.analysis.measure]
    SigmaRing.Exports.measure_SigmaRing__to__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
    SigmaRing.Exports.measure_SigmaRing_class__to__choice_Choice_class [def, in mathcomp.analysis.measure]
    SigmaRing.Exports.measure_SigmaRing_class__to__classical_sets_Pointed_class [def, in mathcomp.analysis.measure]
    SigmaRing.Exports.measure_SigmaRing_class__to__eqtype_Equality_class [def, in mathcomp.analysis.measure]
    SigmaRing.Exports.measure_SigmaRing_class__to__measure_RingOfSets_class [def, in mathcomp.analysis.measure]
    SigmaRing.Exports.measure_SigmaRing_class__to__measure_SemiRingOfSets_class [def, in mathcomp.analysis.measure]
    SigmaRing.measure_hasMeasurableCountableUnion_mixin [proj, in mathcomp.analysis.measure]
    SigmaRing.measure_isSemiRingOfSets_mixin [proj, in mathcomp.analysis.measure]
    SigmaRing.measure_SemiRingOfSets_isRingOfSets_mixin [proj, in mathcomp.analysis.measure]
    SigmaRing.pack_ [def, in mathcomp.analysis.measure]
    SigmaRing.phant_clone [def, in mathcomp.analysis.measure]
    SigmaRing.phant_on_ [def, in mathcomp.analysis.measure]
    SigmaRing.sort [proj, in mathcomp.analysis.measure]
    SigmaRing.type [rec, in mathcomp.analysis.measure]
    sigmaring_lemmas.d [var, in mathcomp.analysis.measure]
    sigmaring_lemmas.T [var, in mathcomp.analysis.measure]
    SigmaRingElpiOperations [mod, in mathcomp.analysis.measure]
    sigmaRingType_lambda_system [prf, in mathcomp.analysis.measure]
    signed [file, in mathcomp.reals.signed]
    Signed [mod, in mathcomp.reals.signed]
    Signed.allP [proj, in mathcomp.reals.signed]
    Signed.def [rec, in mathcomp.reals.signed]
    Signed.Exports [mod, in mathcomp.reals.signed]
    [ sgn of ] [not, in mathcomp.reals.signed] (in ring_scope)
    { nonneg } [not, in mathcomp.reals.signed] (in ring_scope)
    { num & & } [not, in mathcomp.reals.signed] (in ring_scope)
    { posnum } [not, in mathcomp.reals.signed] (in ring_scope)
    %:nngnum [not, in mathcomp.reals.signed] (in ring_scope)
    %:num [not, in mathcomp.reals.signed] (in ring_scope)
    %:posnum [not, in mathcomp.reals.signed] (in ring_scope)
    %:sgn [not, in mathcomp.reals.signed] (in ring_scope)
    !=0 [not, in mathcomp.reals.signed] (in snum_nullity_scope)
    ?=0 [not, in mathcomp.reals.signed] (in snum_nullity_scope)
    <=0 [not, in mathcomp.reals.signed] (in snum_sign_scope)
    =0 [not, in mathcomp.reals.signed] (in snum_sign_scope)
    >=0 [not, in mathcomp.reals.signed] (in snum_sign_scope)
    >=<0 [not, in mathcomp.reals.signed] (in snum_sign_scope)
    >?<0 [not, in mathcomp.reals.signed] (in snum_sign_scope)
    { != : } [not, in mathcomp.reals.signed] (in type_scope)
    { != } [not, in mathcomp.reals.signed] (in type_scope)
    { < : } [not, in mathcomp.reals.signed] (in type_scope)
    { < } [not, in mathcomp.reals.signed] (in type_scope)
    { <= : } [not, in mathcomp.reals.signed] (in type_scope)
    { <= } [not, in mathcomp.reals.signed] (in type_scope)
    { = : } [not, in mathcomp.reals.signed] (in type_scope)
    { = } [not, in mathcomp.reals.signed] (in type_scope)
    { > : } [not, in mathcomp.reals.signed] (in type_scope)
    { > } [not, in mathcomp.reals.signed] (in type_scope)
    { >< : } [not, in mathcomp.reals.signed] (in type_scope)
    { >< } [not, in mathcomp.reals.signed] (in type_scope)
    { >= : } [not, in mathcomp.reals.signed] (in type_scope)
    { >= } [not, in mathcomp.reals.signed] (in type_scope)
    { >=< : } [not, in mathcomp.reals.signed] (in type_scope)
    { >=< } [not, in mathcomp.reals.signed] (in type_scope)
    { ?= : } [not, in mathcomp.reals.signed] (in type_scope)
    { ?= } [not, in mathcomp.reals.signed] (in type_scope)
    { compare & & } [not, in mathcomp.reals.signed] (in type_scope)
    Signed.Exports.nonneg [def, in mathcomp.reals.signed]
    Signed.Exports.num [abbrev, in mathcomp.reals.signed]
    Signed.Exports.posnum [def, in mathcomp.reals.signed]
    Signed.from [def, in mathcomp.reals.signed]
    Signed.fromP [def, in mathcomp.reals.signed]
    Signed.is_real [def, in mathcomp.reals.signed]
    Signed.mk [def, in mathcomp.reals.signed]
    Signed.P [proj, in mathcomp.reals.signed]
    Signed.r [proj, in mathcomp.reals.signed]
    Signed.reality_cond [def, in mathcomp.reals.signed]
    Signed.Signed.disp [var, in mathcomp.reals.signed]
    Signed.Signed.T [var, in mathcomp.reals.signed]
    Signed.Signed.x0 [var, in mathcomp.reals.signed]
    Signed.sort [proj, in mathcomp.reals.signed]
    Signed.sort_x0 [proj, in mathcomp.reals.signed]
    Signed.spec [abbrev, in mathcomp.reals.signed]
    Signed.typ [rec, in mathcomp.reals.signed]
    Signed_def__canonical__choice_Choice [def, in mathcomp.reals.signed]
    Signed_def__canonical__choice_SubChoice [def, in mathcomp.reals.signed]
    Signed_def__canonical__eqtype_Equality [def, in mathcomp.reals.signed]
    Signed_def__canonical__eqtype_SubEquality [def, in mathcomp.reals.signed]
    Signed_def__canonical__eqtype_SubType [def, in mathcomp.reals.signed]
    Signed_def__canonical__Order_DistrLattice [def, in mathcomp.reals.signed]
    Signed_def__canonical__Order_Lattice [def, in mathcomp.reals.signed]
    Signed_def__canonical__Order_POrder [def, in mathcomp.reals.signed]
    Signed_def__canonical__Order_Total [def, in mathcomp.reals.signed]
    signed_intro [prf, in mathcomp.reals.signed]
    signed_le_total [prf, in mathcomp.reals.signed]
    SignedNumDomainStability.R [var, in mathcomp.reals.constructive_ereal]
    SignedRealFieldStability.R [var, in mathcomp.analysis.ereal]
    sigR [def, in mathcomp.classical.functions]
    sigR_funK [prf, in mathcomp.classical.functions]
    sigR_inj_subproof [prf, in mathcomp.classical.functions]
    sigR_some_inv [prf, in mathcomp.classical.functions]
    sigR_surj_subproof [prf, in mathcomp.classical.functions]
    sigRK [prf, in mathcomp.classical.functions]
    SigSub [def, in mathcomp.classical.classical_sets]
    sigT_compact [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_continuous [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_fun [def, in mathcomp.classical.mathcomp_extra]
    sigT_hausdorff [prf, in mathcomp.analysis.separation_axioms]
    sigT_nbhs [def, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_nbhs_nbhs [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_nbhs_proper [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_nbhs_singleton [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_nbhsE [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_of_setX [def, in mathcomp.analysis.topology_theory.subtype_topology]
    sigT_of_setX_continuous [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    sigT_of_setXK [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    sigT_openP [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_separations.I [var, in mathcomp.analysis.separation_axioms]
    sigT_separations.X [var, in mathcomp.analysis.separation_axioms]
    sigT_setUE [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_topology [file, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_topology.I [var, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_topology.X [var, in mathcomp.analysis.topology_theory.sigT_topology]
    simple_bounded [prf, in mathcomp.analysis.lebesgue_integral]
    simple_bounded.d [var, in mathcomp.analysis.lebesgue_integral]
    simple_bounded.R [var, in mathcomp.analysis.lebesgue_integral]
    simple_bounded.T [var, in mathcomp.analysis.lebesgue_integral]
    simple_density_L1.d [var, in mathcomp.analysis.lebesgue_integral]
    simple_density_L1.E [var, in mathcomp.analysis.lebesgue_integral]
    simple_density_L1.mE [var, in mathcomp.analysis.lebesgue_integral]
    simple_density_L1.mu [var, in mathcomp.analysis.lebesgue_integral]
    simple_density_L1.R [var, in mathcomp.analysis.lebesgue_integral]
    simple_density_L1.sfun_dense_L1_pos [var, in mathcomp.analysis.lebesgue_integral]
    simple_density_L1.T [var, in mathcomp.analysis.lebesgue_integral]
    simple_fun_raw_integral.f [var, in mathcomp.analysis.lebesgue_integral]
    simple_fun_raw_integral.mu [var, in mathcomp.analysis.lebesgue_integral]
    simple_fun_raw_integral.R [var, in mathcomp.analysis.lebesgue_integral]
    simple_fun_raw_integral.T [var, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__choice_Choice [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__choice_SubChoice [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__eqtype_Equality [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__eqtype_SubEquality [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__eqtype_SubType [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__GRing_ComRing [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__GRing_ComSemiRing [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__GRing_Nmodule [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__GRing_Ring [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__GRing_SemiRing [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__GRing_SubComRing [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__GRing_SubComSemiRing [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__GRing_SubNmodule [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__GRing_SubRing [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__GRing_SubSemiRing [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__GRing_SubZmodule [def, in mathcomp.analysis.lebesgue_integral]
    SimpleFun_type__canonical__GRing_Zmodule [def, in mathcomp.analysis.lebesgue_integral]
    simpm [abbrev, in mathcomp.experimental_reals.realsum]
    simpm [abbrev, in mathcomp.experimental_reals.distr]
    sin [mod, in mathcomp.analysis.trigo]
    sin.body [def, in mathcomp.analysis.trigo]
    sin.unlock [def, in mathcomp.analysis.trigo]
    sin0 [prf, in mathcomp.analysis.trigo]
    sin0cos1 [prf, in mathcomp.analysis.trigo]
    sin1cos0 [prf, in mathcomp.analysis.trigo]
    sin2_gt0 [prf, in mathcomp.analysis.trigo]
    sin2cos2 [prf, in mathcomp.analysis.trigo]
    sin2pi [prf, in mathcomp.analysis.trigo]
    sin_acos [prf, in mathcomp.analysis.trigo]
    sin_coeff [def, in mathcomp.analysis.trigo]
    sin_coeff' [def, in mathcomp.analysis.trigo]
    sin_coeff'E [prf, in mathcomp.analysis.trigo]
    sin_coeff_even [prf, in mathcomp.analysis.trigo]
    sin_coeffE [prf, in mathcomp.analysis.trigo]
    sin_ge0_pi [prf, in mathcomp.analysis.trigo]
    sin_geN1 [prf, in mathcomp.analysis.trigo]
    sin_gt0_pi [prf, in mathcomp.analysis.trigo]
    sin_gt0_pihalf [prf, in mathcomp.analysis.trigo]
    sin_inj [prf, in mathcomp.analysis.trigo]
    sin_le1 [prf, in mathcomp.analysis.trigo]
    sin_Locked [modtype, in mathcomp.analysis.trigo]
    sin_Locked.body [ax, in mathcomp.analysis.trigo]
    sin_Locked.unlock [ax, in mathcomp.analysis.trigo]
    sin_max [prf, in mathcomp.analysis.trigo]
    sin_mulr2n [prf, in mathcomp.analysis.trigo]
    sin_pihalf [prf, in mathcomp.analysis.trigo]
    sin_sg [prf, in mathcomp.analysis.trigo]
    sin_unlock_subterm [def, in mathcomp.analysis.trigo]
    sinB [prf, in mathcomp.analysis.trigo]
    sinBpihalf [prf, in mathcomp.analysis.trigo]
    sinD [prf, in mathcomp.reals_stdlib.Rstruct]
    sinD [prf, in mathcomp.analysis.trigo]
    sinD2pi [prf, in mathcomp.analysis.trigo]
    sinD_cosD [prf, in mathcomp.analysis.trigo]
    sinDpi [prf, in mathcomp.analysis.trigo]
    sinDpihalf [prf, in mathcomp.analysis.trigo]
    sinE [prf, in mathcomp.analysis.trigo]
    singletons [def, in mathcomp.analysis.function_spaces]
    sinK [prf, in mathcomp.analysis.trigo]
    sinN [prf, in mathcomp.analysis.trigo]
    sinN_cosN [prf, in mathcomp.analysis.trigo]
    sinpi [prf, in mathcomp.analysis.trigo]
    sintegral [def, in mathcomp.analysis.lebesgue_integral]
    sintegral0 [prf, in mathcomp.analysis.lebesgue_integral]
    sintegral_EFin_cst [prf, in mathcomp.analysis.lebesgue_integral]
    sintegral_ge0 [prf, in mathcomp.analysis.lebesgue_integral]
    sintegral_indic [prf, in mathcomp.analysis.lebesgue_integral]
    sintegral_lemmas.d [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_lemmas.mu [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_lemmas.R [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_lemmas.T [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit.d [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit.f [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit.g [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit.gf [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit.limg [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit.mu [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit.nd_g [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit.R [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit.T [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.bigcup_fleg [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.d [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.f [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.fleg [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.g [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.g1 [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.gf [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.le_ffleg [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.mfleg [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.mu [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.nd_fleg [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.nd_g [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.R [var, in mathcomp.analysis.lebesgue_integral]
    sintegral_nondecreasing_limit_lemma.T [var, in mathcomp.analysis.lebesgue_integral]
    sintegralD [prf, in mathcomp.analysis.lebesgue_integral]
    sintegralD.D [var, in mathcomp.analysis.lebesgue_integral]
    sintegralD.d [var, in mathcomp.analysis.lebesgue_integral]
    sintegralD.f [var, in mathcomp.analysis.lebesgue_integral]
    sintegralD.g [var, in mathcomp.analysis.lebesgue_integral]
    sintegralD.m [var, in mathcomp.analysis.lebesgue_integral]
    sintegralD.mD [var, in mathcomp.analysis.lebesgue_integral]
    sintegralD.R [var, in mathcomp.analysis.lebesgue_integral]
    sintegralD.T [var, in mathcomp.analysis.lebesgue_integral]
    sintegralE [prf, in mathcomp.analysis.lebesgue_integral]
    sintegralEnnsfun [prf, in mathcomp.analysis.lebesgue_integral]
    sintegralET [prf, in mathcomp.analysis.lebesgue_integral]
    sintegralrM [prf, in mathcomp.analysis.lebesgue_integral]
    sintegralrM.d [var, in mathcomp.analysis.lebesgue_integral]
    sintegralrM.f [var, in mathcomp.analysis.lebesgue_integral]
    sintegralrM.m [var, in mathcomp.analysis.lebesgue_integral]
    sintegralrM.r [var, in mathcomp.analysis.lebesgue_integral]
    sintegralrM.R [var, in mathcomp.analysis.lebesgue_integral]
    sintegralrM.T [var, in mathcomp.analysis.lebesgue_integral]
    skew [abbrev, in mathcomp.analysis.forms]
    small_ent_sub [def, in mathcomp.analysis.function_spaces]
    small_set_sub [prf, in mathcomp.classical.filter]
    smallest [def, in mathcomp.classical.classical_sets]
    smallest.C [var, in mathcomp.classical.classical_sets]
    smallest.G [var, in mathcomp.classical.classical_sets]
    smallest.T [var, in mathcomp.classical.classical_sets]
    smallest_filter_filter [inst, in mathcomp.classical.filter]
    smallest_filter_finI [prf, in mathcomp.classical.filter]
    smallest_id [prf, in mathcomp.classical.classical_sets]
    smallest_lambda_system [prf, in mathcomp.analysis.measure]
    smallest_lambda_system.D [var, in mathcomp.analysis.measure]
    smallest_lambda_system.G [var, in mathcomp.analysis.measure]
    smallest_lambda_system.lambdaDG [var, in mathcomp.analysis.measure]
    smallest_lambda_system.setIG [var, in mathcomp.analysis.measure]
    smallest_lambda_system.T [var, in mathcomp.analysis.measure]
    smallest_monotone_classE [abbrev, in mathcomp.analysis.measure]
    smallest_setring [prf, in mathcomp.analysis.measure]
    smallest_sigma_algebra [prf, in mathcomp.analysis.measure]
    smallest_sigma_ring [prf, in mathcomp.analysis.measure]
    smallest_sub [prf, in mathcomp.classical.classical_sets]
    snd_fset [def, in mathcomp.classical.cardinality]
    snd_open [prf, in mathcomp.analysis.topology_theory.product_topology]
    snd_set [def, in mathcomp.classical.classical_sets]
    snd_set_snd [prf, in mathcomp.classical.classical_sets]
    snd_setM [abbrev, in mathcomp.classical.classical_sets]
    snd_setX [prf, in mathcomp.classical.classical_sets]
    Some.A [var, in mathcomp.classical.functions]
    Some.T [var, in mathcomp.classical.functions]
    some_bigcap [prf, in mathcomp.classical.classical_sets]
    some_can_subproof [prf, in mathcomp.classical.functions]
    some_canV_subproof [prf, in mathcomp.classical.functions]
    some_comp_inv [prf, in mathcomp.classical.functions]
    some_fun_subproof [prf, in mathcomp.classical.functions]
    some_image [prf, in mathcomp.classical.classical_sets]
    some_inv [prf, in mathcomp.classical.functions]
    some_inv_glue_subproof [prf, in mathcomp.classical.functions]
    some_iter_inv [prf, in mathcomp.classical.functions]
    some_preimage [prf, in mathcomp.classical.classical_sets]
    some_set0 [prf, in mathcomp.classical.classical_sets]
    some_set1 [prf, in mathcomp.classical.classical_sets]
    some_set_eq0 [prf, in mathcomp.classical.classical_sets]
    some_setC [prf, in mathcomp.classical.classical_sets]
    some_setD [prf, in mathcomp.classical.classical_sets]
    some_setI [prf, in mathcomp.classical.classical_sets]
    some_setT [prf, in mathcomp.classical.classical_sets]
    some_setU [prf, in mathcomp.classical.classical_sets]
    sort__canonical__choice_Choice [def, in mathcomp.classical.boolp]
    sort__canonical__classical_sets_Pointed [def, in mathcomp.classical.classical_sets]
    sort__canonical__eqtype_Equality [def, in mathcomp.classical.boolp]
    Specif_sigT__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.sigT_topology]
    Specif_sigT__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.sigT_topology]
    Specif_sigT__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.sigT_topology]
    split [abbrev, in mathcomp.classical.functions]
    split [abbrev, in mathcomp.classical.functions]
    split.A [var, in mathcomp.classical.functions]
    split.aT [var, in mathcomp.classical.functions]
    split.B [var, in mathcomp.classical.functions]
    split.dflt [var, in mathcomp.classical.functions]
    split.hb_instance_417.f [var, in mathcomp.classical.functions]
    split.hb_instance_429.f [var, in mathcomp.classical.functions]
    split.hb_instance_433.f [var, in mathcomp.classical.functions]
    split.hb_instance_438.f [var, in mathcomp.classical.functions]
    split.hb_instance_444.f [var, in mathcomp.classical.functions]
    split.hb_instance_449.f [var, in mathcomp.classical.functions]
    split.hb_instance_455.f [var, in mathcomp.classical.functions]
    split.oinv.f [var, in mathcomp.classical.functions]
    split.oinv.g [var, in mathcomp.classical.functions]
    split.rT [var, in mathcomp.classical.functions]
    split_ [def, in mathcomp.classical.functions]
    split_ent [def, in mathcomp.analysis.topology_theory.uniform_structure]
    split_ent_subset [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    split_entP [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    SplitBij [mod, in mathcomp.classical.functions]
    SplitBij.axioms_ [rec, in mathcomp.classical.functions]
    SplitBij.class [proj, in mathcomp.classical.functions]
    SplitBij.Exports [mod, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_Bij [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_Fun [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_Inject [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_InjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_Inversible [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_InvFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_OInversible [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_OInvFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_SplitInj [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_SplitInjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_SplitSurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_Surject [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij__to__functions_SurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_Bij_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_Fun_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_Inject_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_InjFun_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_Inversible_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_InvFun_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_OInversible_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_OInvFun_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_SplitInj_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_SplitInjFun_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_SplitSurj_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_SplitSurjFun_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_Surject_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.functions_SplitBij_class__to__functions_SurjFun_class [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_Inversible [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_InvFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_SplitInj [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_SplitInjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Inject_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Inject_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_InjFun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_InjFun_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInj_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInj_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInj_and_functions_Surject [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInj_and_functions_SurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInjFun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInjFun_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInjFun_and_functions_Surject [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInjFun_and_functions_SurjFun [def, in mathcomp.classical.functions]
    SplitBij.functions_isFun_mixin [proj, in mathcomp.classical.functions]
    SplitBij.functions_OInv_Can_mixin [proj, in mathcomp.classical.functions]
    SplitBij.functions_OInv_CanV_mixin [proj, in mathcomp.classical.functions]
    SplitBij.functions_OInv_Inv_mixin [proj, in mathcomp.classical.functions]
    SplitBij.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    SplitBij.pack_ [def, in mathcomp.classical.functions]
    SplitBij.phant_clone [def, in mathcomp.classical.functions]
    SplitBij.phant_on_ [def, in mathcomp.classical.functions]
    SplitBij.sort [proj, in mathcomp.classical.functions]
    SplitBij.type [rec, in mathcomp.classical.functions]
    splitbij_sub [prf, in mathcomp.classical.functions]
    splitbij_sub_sym [prf, in mathcomp.classical.functions]
    SplitBijElpiOperations [mod, in mathcomp.classical.functions]
    splitid [prf, in mathcomp.classical.functions]
    SplitInj [mod, in mathcomp.classical.functions]
    SplitInj.axioms_ [rec, in mathcomp.classical.functions]
    SplitInj.class [proj, in mathcomp.classical.functions]
    SplitInj.Exports [mod, in mathcomp.classical.functions]
    SplitInj.Exports.functions_SplitInj__to__functions_Inject [def, in mathcomp.classical.functions]
    SplitInj.Exports.functions_SplitInj__to__functions_Inversible [def, in mathcomp.classical.functions]
    SplitInj.Exports.functions_SplitInj__to__functions_OInversible [def, in mathcomp.classical.functions]
    SplitInj.Exports.functions_SplitInj_class__to__functions_Inject_class [def, in mathcomp.classical.functions]
    SplitInj.Exports.functions_SplitInj_class__to__functions_Inversible_class [def, in mathcomp.classical.functions]
    SplitInj.Exports.functions_SplitInj_class__to__functions_OInversible_class [def, in mathcomp.classical.functions]
    SplitInj.Exports.join_functions_SplitInj_between_functions_Inject_and_functions_Inversible [def, in mathcomp.classical.functions]
    SplitInj.functions_OInv_Can_mixin [proj, in mathcomp.classical.functions]
    SplitInj.functions_OInv_Inv_mixin [proj, in mathcomp.classical.functions]
    SplitInj.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    SplitInj.pack_ [def, in mathcomp.classical.functions]
    SplitInj.phant_clone [def, in mathcomp.classical.functions]
    SplitInj.phant_on_ [def, in mathcomp.classical.functions]
    SplitInj.sort [proj, in mathcomp.classical.functions]
    SplitInj.type [rec, in mathcomp.classical.functions]
    SplitInjElpiOperations [mod, in mathcomp.classical.functions]
    SplitInjFun [mod, in mathcomp.classical.functions]
    SplitInjFun.axioms_ [rec, in mathcomp.classical.functions]
    SplitInjFun.class [proj, in mathcomp.classical.functions]
    SplitInjFun.Exports [mod, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun__to__functions_Fun [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun__to__functions_Inject [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun__to__functions_InjFun [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun__to__functions_Inversible [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun__to__functions_InvFun [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun__to__functions_OInversible [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun__to__functions_OInvFun [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun__to__functions_SplitInj [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun_class__to__functions_Fun_class [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun_class__to__functions_Inject_class [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun_class__to__functions_InjFun_class [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun_class__to__functions_Inversible_class [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun_class__to__functions_InvFun_class [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun_class__to__functions_OInversible_class [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun_class__to__functions_OInvFun_class [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.functions_SplitInjFun_class__to__functions_SplitInj_class [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_Fun_and_functions_SplitInj [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_Inject_and_functions_InvFun [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_InjFun_and_functions_Inversible [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_InjFun_and_functions_InvFun [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_InjFun_and_functions_SplitInj [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_InvFun_and_functions_SplitInj [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_OInvFun_and_functions_SplitInj [def, in mathcomp.classical.functions]
    SplitInjFun.functions_isFun_mixin [proj, in mathcomp.classical.functions]
    SplitInjFun.functions_OInv_Can_mixin [proj, in mathcomp.classical.functions]
    SplitInjFun.functions_OInv_Inv_mixin [proj, in mathcomp.classical.functions]
    SplitInjFun.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    SplitInjFun.pack_ [def, in mathcomp.classical.functions]
    SplitInjFun.phant_clone [def, in mathcomp.classical.functions]
    SplitInjFun.phant_on_ [def, in mathcomp.classical.functions]
    SplitInjFun.sort [proj, in mathcomp.classical.functions]
    SplitInjFun.type [rec, in mathcomp.classical.functions]
    SplitInjFun_CanV [mod, in mathcomp.classical.functions]
    SplitInjFun_CanV.axioms_ [rec, in mathcomp.classical.functions]
    SplitInjFun_CanV.Exports [mod, in mathcomp.classical.functions]
    SplitInjFun_CanV.injV [proj, in mathcomp.classical.functions]
    SplitInjFun_CanV.invS [proj, in mathcomp.classical.functions]
    SplitInjFun_CanV.phant_axioms [def, in mathcomp.classical.functions]
    SplitInjFun_CanV.phant_Build [def, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV.A [var, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV.aT [var, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV.B [var, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV.f [var, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV.local_mixin_functions_isFun [var, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV.local_mixin_functions_OInv [var, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV.local_mixin_functions_OInv_Can [var, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV.local_mixin_functions_OInv_Inv [var, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV.rT [var, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV_f__canonical__functions_Fun [def, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV_f__canonical__functions_Inject [def, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV_f__canonical__functions_InjFun [def, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV_f__canonical__functions_Inversible [def, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV_f__canonical__functions_InvFun [def, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV_f__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV_f__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
    SplitInjFun_CanV.SplitInjFun_CanV_f__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
    SplitInjFunElpiOperations [mod, in mathcomp.classical.functions]
    splitis_inj_subproof [prf, in mathcomp.classical.functions]
    SplitSurj [mod, in mathcomp.classical.functions]
    SplitSurj.axioms_ [rec, in mathcomp.classical.functions]
    SplitSurj.class [proj, in mathcomp.classical.functions]
    SplitSurj.Exports [mod, in mathcomp.classical.functions]
    SplitSurj.Exports.functions_SplitSurj__to__functions_Inversible [def, in mathcomp.classical.functions]
    SplitSurj.Exports.functions_SplitSurj__to__functions_OInversible [def, in mathcomp.classical.functions]
    SplitSurj.Exports.functions_SplitSurj__to__functions_Surject [def, in mathcomp.classical.functions]
    SplitSurj.Exports.functions_SplitSurj_class__to__functions_Inversible_class [def, in mathcomp.classical.functions]
    SplitSurj.Exports.functions_SplitSurj_class__to__functions_OInversible_class [def, in mathcomp.classical.functions]
    SplitSurj.Exports.functions_SplitSurj_class__to__functions_Surject_class [def, in mathcomp.classical.functions]
    SplitSurj.Exports.join_functions_SplitSurj_between_functions_Inversible_and_functions_Surject [def, in mathcomp.classical.functions]
    SplitSurj.functions_OInv_CanV_mixin [proj, in mathcomp.classical.functions]
    SplitSurj.functions_OInv_Inv_mixin [proj, in mathcomp.classical.functions]
    SplitSurj.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    SplitSurj.pack_ [def, in mathcomp.classical.functions]
    SplitSurj.phant_clone [def, in mathcomp.classical.functions]
    SplitSurj.phant_on_ [def, in mathcomp.classical.functions]
    SplitSurj.sort [proj, in mathcomp.classical.functions]
    SplitSurj.type [rec, in mathcomp.classical.functions]
    splitsurj_subproof [prf, in mathcomp.classical.functions]
    SplitSurjElpiOperations [mod, in mathcomp.classical.functions]
    SplitSurjFun [mod, in mathcomp.classical.functions]
    SplitSurjFun.axioms_ [rec, in mathcomp.classical.functions]
    SplitSurjFun.class [proj, in mathcomp.classical.functions]
    SplitSurjFun.Exports [mod, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun__to__functions_Fun [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun__to__functions_Inversible [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun__to__functions_InvFun [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun__to__functions_OInversible [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun__to__functions_OInvFun [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun__to__functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun__to__functions_Surject [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun__to__functions_SurjFun [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun_class__to__functions_Fun_class [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun_class__to__functions_Inversible_class [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun_class__to__functions_InvFun_class [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun_class__to__functions_OInversible_class [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun_class__to__functions_OInvFun_class [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun_class__to__functions_SplitSurj_class [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun_class__to__functions_Surject_class [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.functions_SplitSurjFun_class__to__functions_SurjFun_class [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_Fun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_Inversible_and_functions_SurjFun [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_InvFun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_InvFun_and_functions_Surject [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_InvFun_and_functions_SurjFun [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_OInvFun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_SplitSurj_and_functions_SurjFun [def, in mathcomp.classical.functions]
    SplitSurjFun.functions_isFun_mixin [proj, in mathcomp.classical.functions]
    SplitSurjFun.functions_OInv_CanV_mixin [proj, in mathcomp.classical.functions]
    SplitSurjFun.functions_OInv_Inv_mixin [proj, in mathcomp.classical.functions]
    SplitSurjFun.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    SplitSurjFun.pack_ [def, in mathcomp.classical.functions]
    SplitSurjFun.phant_clone [def, in mathcomp.classical.functions]
    SplitSurjFun.phant_on_ [def, in mathcomp.classical.functions]
    SplitSurjFun.sort [proj, in mathcomp.classical.functions]
    SplitSurjFun.type [rec, in mathcomp.classical.functions]
    SplitSurjFun_Inj [mod, in mathcomp.classical.functions]
    SplitSurjFun_Inj.axioms_ [rec, in mathcomp.classical.functions]
    SplitSurjFun_Inj.Exports [mod, in mathcomp.classical.functions]
    SplitSurjFun_Inj.inj [proj, in mathcomp.classical.functions]
    SplitSurjFun_Inj.phant_axioms [def, in mathcomp.classical.functions]
    SplitSurjFun_Inj.phant_Build [def, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj.A [var, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj.aT [var, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj.B [var, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj.f [var, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj.local_mixin_functions_isFun [var, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj.local_mixin_functions_OInv [var, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj.local_mixin_functions_OInv_CanV [var, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj.local_mixin_functions_OInv_Inv [var, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj.rT [var, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj_f__canonical__functions_Fun [def, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj_f__canonical__functions_Inversible [def, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj_f__canonical__functions_InvFun [def, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj_f__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj_f__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj_f__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj_f__canonical__functions_Surject [def, in mathcomp.classical.functions]
    SplitSurjFun_Inj.SplitSurjFun_Inj_f__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
    SplitSurjFunElpiOperations [mod, in mathcomp.classical.functions]
    splitV [prf, in mathcomp.classical.functions]
    sprob_kernel [def, in mathcomp.analysis.kernel]
    sprobability_setT [def, in mathcomp.analysis.measure]
    sqr_continuous [prf, in mathcomp.analysis.realfun]
    sqr_sqrte [prf, in mathcomp.reals.constructive_ereal]
    sqre_ge0 [prf, in mathcomp.reals.constructive_ereal]
    sqreD [prf, in mathcomp.reals.constructive_ereal]
    sqrt_continuous [prf, in mathcomp.analysis.realfun]
    sqrt_nonzero_subdef [def, in mathcomp.reals.signed]
    sqrt_snum [def, in mathcomp.reals.signed]
    sqrt_snum_subproof [prf, in mathcomp.reals.signed]
    sqrtC_reality_subdef [def, in mathcomp.reals.signed]
    sqrtC_snum [def, in mathcomp.reals.signed]
    sqrtC_snum_subproof [prf, in mathcomp.reals.signed]
    sqrte [def, in mathcomp.reals.constructive_ereal]
    sqrte.R [var, in mathcomp.reals.constructive_ereal]
    sqrte0 [prf, in mathcomp.reals.constructive_ereal]
    sqrte_fin_num [prf, in mathcomp.reals.constructive_ereal]
    sqrte_ge0 [prf, in mathcomp.reals.constructive_ereal]
    sqrte_sqr [prf, in mathcomp.reals.constructive_ereal]
    sqrteM [prf, in mathcomp.reals.constructive_ereal]
    squash [constr, in mathcomp.classical.classical_sets]
    squashed [ind, in mathcomp.classical.classical_sets]
    squeeze_cvge [prf, in mathcomp.analysis.normedtype]
    squeeze_cvgr [prf, in mathcomp.analysis.normedtype]
    squeeze_fin [prf, in mathcomp.analysis.normedtype]
    ssquash [def, in mathcomp.classical.functions]
    ssreal_struct_contd.bigmaxr.R [var, in mathcomp.reals_stdlib.Rstruct]
    ssreal_struct_contd.neq0_RinvE [var, in mathcomp.reals_stdlib.Rstruct]
    ssrfun_comp__canonical__cardinality_FImFun [def, in mathcomp.classical.cardinality]
    ssrfun_comp__canonical__continuous_path_Path [def, in mathcomp.analysis.homotopy_theory.continuous_path]
    ssrfun_comp__canonical__functions_Bij [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_Fun [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_Inject [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_InjFun [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_Inversible [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_InvFun [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_Surject [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
    ssrfun_comp__canonical__lebesgue_integral_MeasurableFun [def, in mathcomp.analysis.lebesgue_integral]
    ssrfun_comp__canonical__topology_structure_Continuous [def, in mathcomp.analysis.topology_theory.topology_structure]
    ssrfun_idfun__canonical__continuous_path_Path [def, in mathcomp.analysis.homotopy_theory.continuous_path]
    ssrfun_idfun__canonical__functions_Bij [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_Fun [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_Inject [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_InjFun [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_Inversible [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_InvFun [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_Surject [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
    ssrfun_idfun__canonical__lebesgue_stieltjes_measure_Cumulative [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
    ssrfun_idfun__canonical__topology_structure_Continuous [def, in mathcomp.analysis.topology_theory.topology_structure]
    ssrfun_olift__canonical__functions_Bij [def, in mathcomp.classical.functions]
    ssrfun_olift__canonical__functions_Fun [def, in mathcomp.classical.functions]
    ssrfun_olift__canonical__functions_Inject [def, in mathcomp.classical.functions]
    ssrfun_olift__canonical__functions_InjFun [def, in mathcomp.classical.functions]
    ssrfun_olift__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    ssrfun_olift__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
    ssrfun_olift__canonical__functions_Surject [def, in mathcomp.classical.functions]
    ssrfun_olift__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_Bij [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_Fun [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_Inject [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_InjFun [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_Inversible [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_InvFun [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_SplitBij [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_SplitInj [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_SplitInjFun [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_SplitSurj [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_SplitSurjFun [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_Surject [def, in mathcomp.classical.functions]
    ssrnat_iter__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
    sT [abbrev, in mathcomp.reals.signed]
    sT [abbrev, in mathcomp.reals.signed]
    sT [abbrev, in mathcomp.reals.signed]
    sT [abbrev, in mathcomp.reals.itv]
    standard_add_continuous [prf, in mathcomp.analysis.tvs]
    standard_emeasurable_fun.R [var, in mathcomp.analysis.lebesgue_measure]
    standard_locally_convex [prf, in mathcomp.analysis.tvs]
    standard_measurable_fun.R [var, in mathcomp.analysis.lebesgue_measure]
    standard_scale_continuous [prf, in mathcomp.analysis.tvs]
    standard_topology.R [var, in mathcomp.analysis.tvs]
    standard_topology.R [var, in mathcomp.analysis.normedtype]
    start_with [def, in mathcomp.classical.classical_orders]
    start_with_prefix [prf, in mathcomp.classical.classical_orders]
    \dlet_ ( <- ) [not, in mathcomp.experimental_reals.distr] (no scope)
    \dlim_ ( ) [not, in mathcomp.experimental_reals.distr] (no scope)
    Std.Bind.f [var, in mathcomp.experimental_reals.distr]
    Std.Bind.mu [var, in mathcomp.experimental_reals.distr]
    Std.Bind.T [var, in mathcomp.experimental_reals.distr]
    Std.Bind.U [var, in mathcomp.experimental_reals.distr]
    Std.BindTheory.T [var, in mathcomp.experimental_reals.distr]
    Std.BindTheory.U [var, in mathcomp.experimental_reals.distr]
    Std.DLetAlg.mu [var, in mathcomp.experimental_reals.distr]
    Std.DLetAlg.mu1 [var, in mathcomp.experimental_reals.distr]
    Std.DLetAlg.mu2 [var, in mathcomp.experimental_reals.distr]
    Std.DLetAlg.T [var, in mathcomp.experimental_reals.distr]
    Std.DLetAlg.U [var, in mathcomp.experimental_reals.distr]
    Std.DLetDLet.f1 [var, in mathcomp.experimental_reals.distr]
    Std.DLetDLet.f2 [var, in mathcomp.experimental_reals.distr]
    Std.DLetDLet.T [var, in mathcomp.experimental_reals.distr]
    Std.DLetDLet.U [var, in mathcomp.experimental_reals.distr]
    Std.DLetDLet.V [var, in mathcomp.experimental_reals.distr]
    Std.DLimTheory.T [var, in mathcomp.experimental_reals.distr]
    Std.DLimTheory.U [var, in mathcomp.experimental_reals.distr]
    Std.Marginals.h [var, in mathcomp.experimental_reals.distr]
    Std.Marginals.mu [var, in mathcomp.experimental_reals.distr]
    Std.Marginals.T [var, in mathcomp.experimental_reals.distr]
    Std.Marginals.U [var, in mathcomp.experimental_reals.distr]
    Std.MarginalsTh.T [var, in mathcomp.experimental_reals.distr]
    Std.MarginalsTh.U [var, in mathcomp.experimental_reals.distr]
    Std.MarginalsTh.V [var, in mathcomp.experimental_reals.distr]
    Std.R [var, in mathcomp.experimental_reals.distr]
    StdDefs.R [var, in mathcomp.experimental_reals.distr]
    StdDefs.T [var, in mathcomp.experimental_reals.distr]
    StdSum.I [var, in mathcomp.experimental_reals.realsum]
    StdSum.R [var, in mathcomp.experimental_reals.realsum]
    StdSum.T [var, in mathcomp.experimental_reals.realsum]
    strace [def, in mathcomp.analysis.measure]
    strace_sigma_ring [prf, in mathcomp.analysis.measure]
    strictly_dominated_by [def, in mathcomp.analysis.normedtype]
    strictly_dominated_by1 [prf, in mathcomp.analysis.normedtype]
    sub0e [prf, in mathcomp.reals.constructive_ereal]
    sub0set [prf, in mathcomp.classical.classical_sets]
    sub1_scale_ball [prf, in mathcomp.analysis.normedtype]
    sub1set [prf, in mathcomp.classical.classical_sets]
    sub_additive [abbrev, in mathcomp.analysis.measure]
    sub_bigcap [prf, in mathcomp.classical.classical_sets]
    sub_boundedl [prf, in mathcomp.analysis.normedtype]
    sub_boundedr [prf, in mathcomp.analysis.normedtype]
    sub_caratheodory [prf, in mathcomp.analysis.measure]
    sub_countable [prf, in mathcomp.classical.cardinality]
    sub_dominatedl [prf, in mathcomp.analysis.normedtype]
    sub_dominatedr [prf, in mathcomp.analysis.normedtype]
    sub_double_eseries [prf, in mathcomp.analysis.sequences]
    sub_double_series [prf, in mathcomp.analysis.sequences]
    sub_eseries [prf, in mathcomp.analysis.sequences]
    sub_eseries_geq [prf, in mathcomp.analysis.sequences]
    sub_finite_set [prf, in mathcomp.classical.cardinality]
    sub_g_sigma_ring [prf, in mathcomp.analysis.measure]
    sub_gen_smallest [prf, in mathcomp.classical.classical_sets]
    sub_image_setI [prf, in mathcomp.classical.classical_sets]
    sub_image_some [prf, in mathcomp.classical.classical_sets]
    sub_image_someP [prf, in mathcomp.classical.classical_sets]
    sub_klipschitz [def, in mathcomp.analysis.normedtype]
    sub_lipschitz [def, in mathcomp.analysis.normedtype]
    sub_meets [prf, in mathcomp.classical.classical_sets]
    sub_Rhull [prf, in mathcomp.analysis.normedtype]
    sub_scale_ball [prf, in mathcomp.analysis.normedtype]
    sub_series [prf, in mathcomp.analysis.sequences]
    sub_series_geq [prf, in mathcomp.analysis.sequences]
    sub_setP [prf, in mathcomp.classical.cardinality]
    sub_setring [prf, in mathcomp.analysis.measure]
    sub_setring2 [prf, in mathcomp.analysis.measure]
    sub_sfun_fimfun [prf, in mathcomp.analysis.lebesgue_integral]
    sub_sfun_mfun [prf, in mathcomp.analysis.lebesgue_integral]
    sub_sigma_algebra [prf, in mathcomp.analysis.measure]
    sub_sigma_algebra2 [prf, in mathcomp.analysis.measure]
    sub_smallest [prf, in mathcomp.classical.classical_sets]
    sub_smallest2l [prf, in mathcomp.classical.classical_sets]
    sub_smallest2r [prf, in mathcomp.classical.classical_sets]
    sub_trivIset [prf, in mathcomp.classical.classical_sets]
    sub_within [prf, in mathcomp.classical.wochoice]
    subadditive [def, in mathcomp.analysis.measure]
    subadditive_countable.d [var, in mathcomp.analysis.lebesgue_integral]
    subadditive_countable.mu [var, in mathcomp.analysis.lebesgue_integral]
    subadditive_countable.R [var, in mathcomp.analysis.lebesgue_integral]
    subadditive_countable.T [var, in mathcomp.analysis.lebesgue_integral]
    subclosed_compact [prf, in mathcomp.analysis.topology_theory.compact]
    subDsetl [prf, in mathcomp.classical.classical_sets]
    subDsetr [prf, in mathcomp.classical.classical_sets]
    sube0 [prf, in mathcomp.reals.constructive_ereal]
    sube_eq [prf, in mathcomp.reals.constructive_ereal]
    sube_ge0 [prf, in mathcomp.reals.constructive_ereal]
    sube_gt0 [prf, in mathcomp.reals.constructive_ereal]
    sube_le0 [prf, in mathcomp.reals.constructive_ereal]
    sube_lt0 [prf, in mathcomp.reals.constructive_ereal]
    subee [prf, in mathcomp.reals.constructive_ereal]
    subeK [prf, in mathcomp.reals.constructive_ereal]
    suber_ge0 [prf, in mathcomp.reals.constructive_ereal]
    suber_lt0 [prf, in mathcomp.reals.constructive_ereal]
    subfun [def, in mathcomp.classical.functions]
    subfun.A [var, in mathcomp.classical.functions]
    subfun.B [var, in mathcomp.classical.functions]
    subfun.hb_instance_784.AB [var, in mathcomp.classical.functions]
    subfun.hb_instance_792.AB [var, in mathcomp.classical.functions]
    subfun.T [var, in mathcomp.classical.functions]
    subfun_eq.A [var, in mathcomp.classical.functions]
    subfun_eq.B [var, in mathcomp.classical.functions]
    subfun_eq.hb_instance_797.AB [var, in mathcomp.classical.functions]
    subfun_eq.T [var, in mathcomp.classical.functions]
    subfun_imageT [prf, in mathcomp.classical.functions]
    subfun_inj [prf, in mathcomp.classical.functions]
    subfun_inv_subproof [prf, in mathcomp.classical.functions]
    subimageK [prf, in mathcomp.classical.classical_sets]
    subIset [prf, in mathcomp.classical.classical_sets]
    subIsetl [prf, in mathcomp.classical.classical_sets]
    subIsetr [prf, in mathcomp.classical.classical_sets]
    subKimage [prf, in mathcomp.classical.classical_sets]
    subl_surj [prf, in mathcomp.classical.functions]
    SubProbability [mod, in mathcomp.analysis.measure]
    SubProbability.axioms_ [rec, in mathcomp.analysis.measure]
    SubProbability.class [proj, in mathcomp.analysis.measure]
    SubProbability.Exports [mod, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability__to__measure_Content [def, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability__to__measure_FiniteMeasure [def, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability__to__measure_FinNumFun [def, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability__to__measure_Measure [def, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability__to__measure_SFiniteMeasure [def, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability__to__measure_SigmaFiniteContent [def, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability__to__measure_SigmaFiniteMeasure [def, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability_class__to__measure_Content_class [def, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability_class__to__measure_FiniteMeasure_class [def, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability_class__to__measure_FinNumFun_class [def, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability_class__to__measure_Measure_class [def, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability_class__to__measure_SFiniteMeasure_class [def, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability_class__to__measure_SigmaFiniteContent_class [def, in mathcomp.analysis.measure]
    SubProbability.Exports.measure_SubProbability_class__to__measure_SigmaFiniteMeasure_class [def, in mathcomp.analysis.measure]
    SubProbability.measure_Content_isMeasure_mixin [proj, in mathcomp.analysis.measure]
    SubProbability.measure_isContent_mixin [proj, in mathcomp.analysis.measure]
    SubProbability.measure_isFinite_mixin [proj, in mathcomp.analysis.measure]
    SubProbability.measure_isSFinite_mixin [proj, in mathcomp.analysis.measure]
    SubProbability.measure_isSigmaFinite_mixin [proj, in mathcomp.analysis.measure]
    SubProbability.measure_isSubProbability_mixin [proj, in mathcomp.analysis.measure]
    SubProbability.pack_ [def, in mathcomp.analysis.measure]
    SubProbability.phant_clone [def, in mathcomp.analysis.measure]
    SubProbability.phant_on_ [def, in mathcomp.analysis.measure]
    SubProbability.sort [proj, in mathcomp.analysis.measure]
    SubProbability.type [rec, in mathcomp.analysis.measure]
    SubProbability_isProbability [mod, in mathcomp.analysis.kernel]
    SubProbability_isProbability.axioms_ [rec, in mathcomp.analysis.kernel]
    SubProbability_isProbability.Exports [mod, in mathcomp.analysis.kernel]
    SubProbability_isProbability.identity_builder [def, in mathcomp.analysis.kernel]
    SubProbability_isProbability.phant_axioms [def, in mathcomp.analysis.kernel]
    SubProbability_isProbability.phant_Build [def, in mathcomp.analysis.kernel]
    SubProbability_isProbability.prob_kernel [proj, in mathcomp.analysis.kernel]
    SubProbability_isProbability.SubProbability_isProbability.d [var, in mathcomp.analysis.kernel]
    SubProbability_isProbability.SubProbability_isProbability.d' [var, in mathcomp.analysis.kernel]
    SubProbability_isProbability.SubProbability_isProbability.k [var, in mathcomp.analysis.kernel]
    SubProbability_isProbability.SubProbability_isProbability.R [var, in mathcomp.analysis.kernel]
    SubProbability_isProbability.SubProbability_isProbability.X [var, in mathcomp.analysis.kernel]
    SubProbability_isProbability.SubProbability_isProbability.Y [var, in mathcomp.analysis.kernel]
    SubProbabilityElpiOperations [mod, in mathcomp.analysis.measure]
    SubProbabilityKernel [mod, in mathcomp.analysis.kernel]
    SubProbabilityKernel.axioms_ [rec, in mathcomp.analysis.kernel]
    SubProbabilityKernel.class [proj, in mathcomp.analysis.kernel]
    SubProbabilityKernel.Exports [mod, in mathcomp.analysis.kernel]
    SubProbabilityKernel.Exports.kernel_SubProbabilityKernel__to__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
    SubProbabilityKernel.Exports.kernel_SubProbabilityKernel__to__kernel_Kernel [def, in mathcomp.analysis.kernel]
    SubProbabilityKernel.Exports.kernel_SubProbabilityKernel__to__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
    SubProbabilityKernel.Exports.kernel_SubProbabilityKernel_class__to__kernel_FiniteKernel_class [def, in mathcomp.analysis.kernel]
    SubProbabilityKernel.Exports.kernel_SubProbabilityKernel_class__to__kernel_Kernel_class [def, in mathcomp.analysis.kernel]
    SubProbabilityKernel.Exports.kernel_SubProbabilityKernel_class__to__kernel_SFiniteKernel_class [def, in mathcomp.analysis.kernel]
    SubProbabilityKernel.kernel_FiniteKernel_isSubProbability_mixin [proj, in mathcomp.analysis.kernel]
    SubProbabilityKernel.kernel_isKernel_mixin [proj, in mathcomp.analysis.kernel]
    SubProbabilityKernel.kernel_Kernel_isSFinite_subdef_mixin [proj, in mathcomp.analysis.kernel]
    SubProbabilityKernel.kernel_SFiniteKernel_isFinite_mixin [proj, in mathcomp.analysis.kernel]
    SubProbabilityKernel.pack_ [def, in mathcomp.analysis.kernel]
    SubProbabilityKernel.phant_clone [def, in mathcomp.analysis.kernel]
    SubProbabilityKernel.phant_on_ [def, in mathcomp.analysis.kernel]
    SubProbabilityKernel.sort [proj, in mathcomp.analysis.kernel]
    SubProbabilityKernel.type [rec, in mathcomp.analysis.kernel]
    SubProbabilityKernelElpiOperations [mod, in mathcomp.analysis.kernel]
    subr_image.R [var, in mathcomp.reals.reals]
    subr_image.R [var, in mathcomp.classical.set_interval]
    subr_surj [prf, in mathcomp.classical.functions]
    subre_ge0 [prf, in mathcomp.reals.constructive_ereal]
    subre_lt0 [prf, in mathcomp.reals.constructive_ereal]
    subset [def, in mathcomp.classical.classical_sets]
    subset0 [prf, in mathcomp.classical.classical_sets]
    subset_ball_prop_in_itv [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    subset_ball_prop_in_itvcc [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    subset_bigcap [prf, in mathcomp.classical.classical_sets]
    subset_bigcap_r [prf, in mathcomp.classical.classical_sets]
    subset_bigcup [prf, in mathcomp.classical.classical_sets]
    subset_bigcup_r [prf, in mathcomp.classical.classical_sets]
    subset_bigsetI [prf, in mathcomp.classical.classical_sets]
    subset_bigsetI_cond [prf, in mathcomp.classical.classical_sets]
    subset_bigsetU [prf, in mathcomp.classical.classical_sets]
    subset_bigsetU_cond [prf, in mathcomp.classical.classical_sets]
    subset_card_le [prf, in mathcomp.classical.cardinality]
    subset_closed_ball [prf, in mathcomp.analysis.normedtype]
    subset_closure [prf, in mathcomp.analysis.topology_theory.topology_structure]
    subset_closure_half [prf, in mathcomp.analysis.normedtype]
    subset_filter [def, in mathcomp.classical.filter]
    subset_filter_filter [inst, in mathcomp.classical.filter]
    subset_filter_proper [prf, in mathcomp.classical.filter]
    subset_fst_set [prf, in mathcomp.classical.classical_sets]
    subset_has_lbound [prf, in mathcomp.classical.classical_sets]
    subset_has_ubound [prf, in mathcomp.classical.classical_sets]
    subset_integral.d [var, in mathcomp.analysis.lebesgue_integral]
    subset_integral.mu [var, in mathcomp.analysis.lebesgue_integral]
    subset_integral.R [var, in mathcomp.analysis.lebesgue_integral]
    subset_integral.T [var, in mathcomp.analysis.lebesgue_integral]
    subset_itvl [prf, in mathcomp.classical.set_interval]
    subset_itvP [prf, in mathcomp.classical.set_interval]
    subset_itvr [prf, in mathcomp.classical.set_interval]
    subset_itvS [abbrev, in mathcomp.classical.set_interval]
    subset_itvScc [prf, in mathcomp.classical.set_interval]
    subset_itvSoo [prf, in mathcomp.classical.set_interval]
    subset_itvW [prf, in mathcomp.classical.set_interval]
    subset_lee_nneseries [prf, in mathcomp.analysis.sequences]
    subset_limit_point [prf, in mathcomp.analysis.topology_theory.topology_structure]
    subset_measure0 [prf, in mathcomp.analysis.measure]
    subset_nonempty [prf, in mathcomp.classical.classical_sets]
    subset_pr [prf, in mathcomp.experimental_reals.distr]
    subset_refl [prf, in mathcomp.classical.classical_sets]
    subset_set1 [prf, in mathcomp.classical.classical_sets]
    subset_set2 [prf, in mathcomp.classical.classical_sets]
    subset_sigma_subadditive [def, in mathcomp.analysis.measure]
    subset_snd_set [prf, in mathcomp.classical.classical_sets]
    subset_split_ent [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    subset_strace [prf, in mathcomp.analysis.measure]
    subset_trans [prf, in mathcomp.classical.classical_sets]
    subsetC [prf, in mathcomp.classical.classical_sets]
    subsetC1 [prf, in mathcomp.classical.classical_sets]
    subsetC2 [prf, in mathcomp.classical.classical_sets]
    subsetC_trivIset [prf, in mathcomp.classical.classical_sets]
    subsetCl [prf, in mathcomp.classical.classical_sets]
    subsetCP [prf, in mathcomp.classical.classical_sets]
    subsetCPl [prf, in mathcomp.classical.classical_sets]
    subsetCPr [prf, in mathcomp.classical.classical_sets]
    subsetCr [prf, in mathcomp.classical.classical_sets]
    subsetCW [def, in mathcomp.classical.classical_sets]
    subsetI [prf, in mathcomp.classical.classical_sets]
    subsetI_eq0 [prf, in mathcomp.classical.classical_sets]
    subsetI_neq0 [prf, in mathcomp.classical.classical_sets]
    subsetP [prf, in mathcomp.classical.classical_sets]
    subsets_disjoint [prf, in mathcomp.classical.classical_sets]
    subsetT [prf, in mathcomp.classical.classical_sets]
    subsetUl [prf, in mathcomp.classical.classical_sets]
    subsetUr [prf, in mathcomp.classical.classical_sets]
    subsetW [prf, in mathcomp.classical.classical_sets]
    subspace [def, in mathcomp.analysis.topology_theory.subspace_topology]
    Subspace.A [var, in mathcomp.analysis.topology_theory.subspace_topology]
    Subspace.T [var, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_ball [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_continuous_measurable_fun [prf, in mathcomp.analysis.lebesgue_measure]
    subspace_continuousP [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_cvgP [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_ent [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_eq_continuous [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_filter [inst, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_hausdorff [prf, in mathcomp.analysis.separation_axioms]
    subspace_product.A [var, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_product.B [var, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_product.X [var, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_product.Y [var, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_product.Z [var, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_proper_filter [inst, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_sig.A [var, in mathcomp.analysis.topology_theory.subtype_topology]
    subspace_sig.X [var, in mathcomp.analysis.topology_theory.subtype_topology]
    subspace_sigL_continuousP [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    subspace_subtypeP [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    subspace_topology [file, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_topology_subspace__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_topology_subspace__canonical__classical_sets_Pointed [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_topology_subspace__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_topology_subspace__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_topology_subspace__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_topology_subspace__canonical__filter_PointedFiltered [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_topology_subspace__canonical__filter_PointedNbhs [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_topology_subspace__canonical__pseudometric_structure_PseudoMetric [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_topology_subspace__canonical__topology_structure_PointedTopological [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_topology_subspace__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_topology_subspace__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_valL_continuousP [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    subspace_valL_continuousP' [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    SubspacePseudoMetric.A [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspacePseudoMetric.R [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspacePseudoMetric.subspace_pm_ball_center [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspacePseudoMetric.subspace_pm_ball_sym [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspacePseudoMetric.subspace_pm_ball_triangle [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspacePseudoMetric.subspace_pm_entourageE [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspacePseudoMetric.X [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspaceRelative.T [var, in mathcomp.analysis.topology_theory.subspace_topology]
    subspaceT_continuous [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspaceUniform.A [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspaceUniform.Filter_subspace_ent [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspaceUniform.subspace_uniform_entourage_diagonal [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspaceUniform.subspace_uniform_entourage_inv [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspaceUniform.subspace_uniform_entourage_split_ex [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspaceUniform.subspace_uniform_nbhsE [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspaceUniform.X [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspaceWeak.f [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspaceWeak.T [var, in mathcomp.analysis.topology_theory.subspace_topology]
    SubspaceWeak.U [var, in mathcomp.analysis.topology_theory.subspace_topology]
    subTset [prf, in mathcomp.classical.classical_sets]
    SubType.P [var, in mathcomp.classical.functions]
    SubType.sT [var, in mathcomp.classical.functions]
    SubType.T [var, in mathcomp.classical.functions]
    SubType.x0 [var, in mathcomp.classical.functions]
    subtype_setX.A [var, in mathcomp.analysis.topology_theory.subtype_topology]
    subtype_setX.B [var, in mathcomp.analysis.topology_theory.subtype_topology]
    subtype_setX.X [var, in mathcomp.analysis.topology_theory.subtype_topology]
    subtype_setX.Y [var, in mathcomp.analysis.topology_theory.subtype_topology]
    subtype_topology [file, in mathcomp.analysis.topology_theory.subtype_topology]
    subUset [prf, in mathcomp.classical.classical_sets]
    succn_snum [def, in mathcomp.reals.signed]
    succn_snum_subproof [prf, in mathcomp.reals.signed]
    sum [def, in mathcomp.experimental_reals.realsum]
    sum [def, in mathcomp.analysis.showcase.summability]
    Sum.R [var, in mathcomp.experimental_reals.realsum]
    Sum.T [var, in mathcomp.experimental_reals.realsum]
    sum0 [prf, in mathcomp.experimental_reals.realsum]
    sum_enum_prob [prf, in mathcomp.analysis.probability]
    sum_fin_num [prf, in mathcomp.reals.constructive_ereal]
    sum_fin_numP [prf, in mathcomp.reals.constructive_ereal]
    sum_fine [prf, in mathcomp.reals.constructive_ereal]
    sum_finseq [prf, in mathcomp.experimental_reals.realsum]
    sum_ncvg [prf, in mathcomp.experimental_reals.realsum]
    sum_nnsfun [def, in mathcomp.analysis.lebesgue_integral]
    sum_nnsfunE [prf, in mathcomp.analysis.lebesgue_integral]
    sum_seq1 [prf, in mathcomp.experimental_reals.realsum]
    sume_ge0 [prf, in mathcomp.reals.constructive_ereal]
    sume_le0 [prf, in mathcomp.reals.constructive_ereal]
    sumEFin [prf, in mathcomp.reals.constructive_ereal]
    sumeN [prf, in mathcomp.reals.constructive_ereal]
    sumID [prf, in mathcomp.experimental_reals.realsum]
    summability [file, in mathcomp.analysis.showcase.summability]
    summable [def, in mathcomp.experimental_reals.realsum]
    summable [def, in mathcomp.analysis.showcase.summability]
    summable [def, in mathcomp.analysis.esum]
    Summable.f [var, in mathcomp.experimental_reals.realsum]
    Summable.R [var, in mathcomp.experimental_reals.realsum]
    Summable.T [var, in mathcomp.experimental_reals.realsum]
    summable0 [prf, in mathcomp.experimental_reals.realsum]
    summable_abs [prf, in mathcomp.experimental_reals.realsum]
    summable_addrC [prf, in mathcomp.experimental_reals.realsum]
    summable_condl [prf, in mathcomp.experimental_reals.realsum]
    summable_condr [prf, in mathcomp.experimental_reals.realsum]
    summable_countn0 [prf, in mathcomp.experimental_reals.realsum]
    summable_cvg [prf, in mathcomp.analysis.esum]
    summable_eseries [prf, in mathcomp.analysis.esum]
    summable_eseries_esum [prf, in mathcomp.analysis.esum]
    summable_fin [prf, in mathcomp.experimental_reals.realsum]
    summable_fine_sum [prf, in mathcomp.analysis.esum]
    summable_fneg [prf, in mathcomp.experimental_reals.realsum]
    summable_fpos [prf, in mathcomp.experimental_reals.realsum]
    summable_fst [prf, in mathcomp.experimental_reals.distr]
    summable_funeneg [prf, in mathcomp.analysis.esum]
    summable_funepos [prf, in mathcomp.analysis.esum]
    summable_has_exp [prf, in mathcomp.experimental_reals.distr]
    summable_integral_dirac [prf, in mathcomp.analysis.lebesgue_integral]
    summable_lemmas.R [var, in mathcomp.analysis.esum]
    summable_lemmas.T [var, in mathcomp.analysis.esum]
    summable_mlet [prf, in mathcomp.experimental_reals.distr]
    summable_mrat [prf, in mathcomp.experimental_reals.distr]
    summable_mu [prf, in mathcomp.experimental_reals.distr]
    summable_mu_wgtd [prf, in mathcomp.experimental_reals.distr]
    summable_mulrC [prf, in mathcomp.experimental_reals.realsum]
    summable_nat.R [var, in mathcomp.analysis.esum]
    summable_nneseries_lim [prf, in mathcomp.analysis.esum]
    summable_of_bd [prf, in mathcomp.experimental_reals.realsum]
    summable_pinfty [prf, in mathcomp.analysis.esum]
    summable_pr [prf, in mathcomp.experimental_reals.distr]
    summable_seqP [prf, in mathcomp.experimental_reals.realsum]
    summable_snd [prf, in mathcomp.experimental_reals.distr]
    summable_sum [prf, in mathcomp.experimental_reals.realsum]
    summable_sup [prf, in mathcomp.experimental_reals.realsum]
    SummableAlg.I [var, in mathcomp.experimental_reals.realsum]
    SummableAlg.R [var, in mathcomp.experimental_reals.realsum]
    SummableAlg.T [var, in mathcomp.experimental_reals.realsum]
    summableB [prf, in mathcomp.analysis.esum]
    summablebDl [prf, in mathcomp.experimental_reals.realsum]
    summablebDr [prf, in mathcomp.experimental_reals.realsum]
    summablebN [prf, in mathcomp.experimental_reals.realsum]
    SummableCountable.f [var, in mathcomp.experimental_reals.realsum]
    SummableCountable.R [var, in mathcomp.experimental_reals.realsum]
    SummableCountable.T [var, in mathcomp.experimental_reals.realsum]
    summableD [prf, in mathcomp.experimental_reals.realsum]
    summableD [prf, in mathcomp.analysis.esum]
    summableE [prf, in mathcomp.analysis.esum]
    summableM [prf, in mathcomp.experimental_reals.realsum]
    summableMl [prf, in mathcomp.experimental_reals.realsum]
    summableMr [prf, in mathcomp.experimental_reals.realsum]
    summableN [prf, in mathcomp.experimental_reals.realsum]
    summableN [prf, in mathcomp.analysis.esum]
    summableP [prf, in mathcomp.experimental_reals.realsum]
    summableZ [prf, in mathcomp.experimental_reals.realsum]
    summableZr [prf, in mathcomp.experimental_reals.realsum]
    sumN [prf, in mathcomp.experimental_reals.realsum]
    sumr_le0 [prf, in mathcomp.classical.mathcomp_extra]
    sumrfctE [prf, in mathcomp.classical.functions]
    SumTh.R [var, in mathcomp.experimental_reals.realsum]
    SumTh.T [var, in mathcomp.experimental_reals.realsum]
    SumTheory.R [var, in mathcomp.experimental_reals.realsum]
    SumTheory.T [var, in mathcomp.experimental_reals.realsum]
    sumZ [prf, in mathcomp.experimental_reals.realsum]
    sup [def, in mathcomp.reals.reals]
    Sup.R [var, in mathcomp.reals.reals]
    sup0 [prf, in mathcomp.reals.reals]
    sup1 [prf, in mathcomp.reals.reals]
    sup_adherent [prf, in mathcomp.reals.reals]
    sup_adherent_subdef [def, in mathcomp.reals.reals]
    sup_contract_le1 [prf, in mathcomp.analysis.ereal]
    sup_down [prf, in mathcomp.reals.reals]
    sup_ent [def, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_filter [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_inv [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_nbhs [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_refl [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_split [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_gt [prf, in mathcomp.reals.reals]
    sup_in_floor_set [prf, in mathcomp.reals.reals]
    sup_itv [prf, in mathcomp.reals.real_interval]
    sup_itvcc [prf, in mathcomp.reals.real_interval]
    sup_le_ub [prf, in mathcomp.reals.reals]
    sup_open [abbrev, in mathcomp.analysis.function_spaces]
    sup_out [prf, in mathcomp.reals.reals]
    sup_pseudometric [def, in mathcomp.analysis.separation_axioms]
    sup_pseudometric.countable_uniformityT [var, in mathcomp.analysis.separation_axioms]
    sup_pseudometric.Icnt [var, in mathcomp.analysis.separation_axioms]
    sup_pseudometric.Ii [var, in mathcomp.analysis.separation_axioms]
    sup_pseudometric.R [var, in mathcomp.analysis.separation_axioms]
    sup_pseudometric.T [var, in mathcomp.analysis.separation_axioms]
    sup_pseudometric.Tc [var, in mathcomp.analysis.separation_axioms]
    sup_pseudometric.TS [var, in mathcomp.analysis.separation_axioms]
    sup_setU [prf, in mathcomp.reals.reals]
    sup_subbase [def, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_sum.R [var, in mathcomp.reals.reals]
    sup_sumE [prf, in mathcomp.reals.reals]
    sup_topology [def, in mathcomp.analysis.topology_theory.supremum_topology]
    Sup_Topology.I [var, in mathcomp.analysis.topology_theory.supremum_topology]
    Sup_Topology.T [var, in mathcomp.analysis.topology_theory.supremum_topology]
    Sup_Topology.Tc [var, in mathcomp.analysis.topology_theory.supremum_topology]
    Sup_Topology.TS [var, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_total [prf, in mathcomp.reals.reals]
    sup_ub [abbrev, in mathcomp.reals.reals]
    sup_ub_strict [prf, in mathcomp.reals.reals]
    sup_ubound [prf, in mathcomp.reals.reals]
    sup_uniform.ent_of [var, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_uniform.I [var, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_uniform.IEnt [var, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_uniform.IEntType [var, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_uniform.Ii [var, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_uniform.T [var, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_uniform.Tc [var, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_uniform.TS [var, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_upper_bound [prf, in mathcomp.reals.reals]
    sup_upper_bound_subdef [def, in mathcomp.reals.reals]
    super_bij [prf, in mathcomp.classical.cardinality]
    SupInterchange.R [var, in mathcomp.experimental_reals.realsum]
    SupInterchange.T [var, in mathcomp.experimental_reals.realsum]
    SupInterchange.U [var, in mathcomp.experimental_reals.realsum]
    supremum [def, in mathcomp.classical.classical_sets]
    supremum0 [prf, in mathcomp.classical.classical_sets]
    supremum1 [prf, in mathcomp.classical.classical_sets]
    supremum_out [prf, in mathcomp.classical.classical_sets]
    supremum_pinfty [prf, in mathcomp.analysis.ereal]
    supremum_topology [file, in mathcomp.analysis.topology_theory.supremum_topology]
    supremum_topology_sup_topology__canonical__choice_Choice [def, in mathcomp.analysis.topology_theory.supremum_topology]
    supremum_topology_sup_topology__canonical__classical_sets_Pointed [def, in mathcomp.analysis.topology_theory.supremum_topology]
    supremum_topology_sup_topology__canonical__eqtype_Equality [def, in mathcomp.analysis.topology_theory.supremum_topology]
    supremum_topology_sup_topology__canonical__filter_Filtered [def, in mathcomp.analysis.topology_theory.supremum_topology]
    supremum_topology_sup_topology__canonical__filter_Nbhs [def, in mathcomp.analysis.topology_theory.supremum_topology]
    supremum_topology_sup_topology__canonical__filter_PointedFiltered [def, in mathcomp.analysis.topology_theory.supremum_topology]
    supremum_topology_sup_topology__canonical__filter_PointedNbhs [def, in mathcomp.analysis.topology_theory.supremum_topology]
    supremum_topology_sup_topology__canonical__topology_structure_PointedTopological [def, in mathcomp.analysis.topology_theory.supremum_topology]
    supremum_topology_sup_topology__canonical__topology_structure_Topological [def, in mathcomp.analysis.topology_theory.supremum_topology]
    supremum_topology_sup_topology__canonical__uniform_structure_Uniform [def, in mathcomp.analysis.topology_theory.supremum_topology]
    supremums [def, in mathcomp.classical.classical_sets]
    supremums1 [prf, in mathcomp.classical.classical_sets]
    supremumsT [prf, in mathcomp.analysis.ereal]
    supremumT [prf, in mathcomp.analysis.ereal]
    sups [def, in mathcomp.analysis.sequences]
    sups_infs.R [var, in mathcomp.analysis.sequences]
    sups_preimage [prf, in mathcomp.analysis.sequences]
    supsN [prf, in mathcomp.analysis.sequences]
    surj [prf, in mathcomp.classical.functions]
    surj_card_ge [prf, in mathcomp.classical.cardinality]
    surj_comp [prf, in mathcomp.classical.functions]
    surj_epi [prf, in mathcomp.classical.functions]
    surj_id [prf, in mathcomp.classical.functions]
    surj_image_eq [prf, in mathcomp.classical.functions]
    surj_lemmas.aT [var, in mathcomp.classical.functions]
    surj_lemmas.rT [var, in mathcomp.classical.functions]
    surj_oinv.A [var, in mathcomp.classical.functions]
    surj_oinv.aT [var, in mathcomp.classical.functions]
    surj_oinv.B [var, in mathcomp.classical.functions]
    surj_oinv.f [var, in mathcomp.classical.functions]
    surj_oinv.fsurj [var, in mathcomp.classical.functions]
    surj_oinv.rT [var, in mathcomp.classical.functions]
    surj_oinv.surjective_oinv [var, in mathcomp.classical.functions]
    surj_set0 [prf, in mathcomp.classical.functions]
    surjE [prf, in mathcomp.classical.functions]
    Surject [mod, in mathcomp.classical.functions]
    Surject.axioms_ [rec, in mathcomp.classical.functions]
    Surject.class [proj, in mathcomp.classical.functions]
    Surject.Exports [mod, in mathcomp.classical.functions]
    Surject.Exports.functions_Surject__to__functions_OInversible [def, in mathcomp.classical.functions]
    Surject.Exports.functions_Surject_class__to__functions_OInversible_class [def, in mathcomp.classical.functions]
    Surject.functions_OInv_CanV_mixin [proj, in mathcomp.classical.functions]
    Surject.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    Surject.pack_ [def, in mathcomp.classical.functions]
    Surject.phant_clone [def, in mathcomp.classical.functions]
    Surject.phant_on_ [def, in mathcomp.classical.functions]
    Surject.sort [proj, in mathcomp.classical.functions]
    Surject.type [rec, in mathcomp.classical.functions]
    SurjectElpiOperations [mod, in mathcomp.classical.functions]
    surjection_of_surj [def, in mathcomp.classical.functions]
    surjective_existT [prf, in mathcomp.classical.boolp]
    surjective_ocanV [def, in mathcomp.classical.functions]
    surjective_oinvK [prf, in mathcomp.classical.functions]
    surjective_oinvS [prf, in mathcomp.classical.functions]
    SurjFun [mod, in mathcomp.classical.functions]
    SurjFun.axioms_ [rec, in mathcomp.classical.functions]
    SurjFun.class [proj, in mathcomp.classical.functions]
    SurjFun.Exports [mod, in mathcomp.classical.functions]
    SurjFun.Exports.functions_SurjFun__to__functions_Fun [def, in mathcomp.classical.functions]
    SurjFun.Exports.functions_SurjFun__to__functions_OInversible [def, in mathcomp.classical.functions]
    SurjFun.Exports.functions_SurjFun__to__functions_OInvFun [def, in mathcomp.classical.functions]
    SurjFun.Exports.functions_SurjFun__to__functions_Surject [def, in mathcomp.classical.functions]
    SurjFun.Exports.functions_SurjFun_class__to__functions_Fun_class [def, in mathcomp.classical.functions]
    SurjFun.Exports.functions_SurjFun_class__to__functions_OInversible_class [def, in mathcomp.classical.functions]
    SurjFun.Exports.functions_SurjFun_class__to__functions_OInvFun_class [def, in mathcomp.classical.functions]
    SurjFun.Exports.functions_SurjFun_class__to__functions_Surject_class [def, in mathcomp.classical.functions]
    SurjFun.Exports.join_functions_SurjFun_between_functions_Fun_and_functions_Surject [def, in mathcomp.classical.functions]
    SurjFun.Exports.join_functions_SurjFun_between_functions_OInvFun_and_functions_Surject [def, in mathcomp.classical.functions]
    SurjFun.functions_isFun_mixin [proj, in mathcomp.classical.functions]
    SurjFun.functions_OInv_CanV_mixin [proj, in mathcomp.classical.functions]
    SurjFun.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    SurjFun.pack_ [def, in mathcomp.classical.functions]
    SurjFun.phant_clone [def, in mathcomp.classical.functions]
    SurjFun.phant_on_ [def, in mathcomp.classical.functions]
    SurjFun.sort [proj, in mathcomp.classical.functions]
    SurjFun.type [rec, in mathcomp.classical.functions]
    SurjFun_Inj [mod, in mathcomp.classical.functions]
    SurjFun_Inj.axioms_ [rec, in mathcomp.classical.functions]
    SurjFun_Inj.Exports [mod, in mathcomp.classical.functions]
    SurjFun_Inj.inj [proj, in mathcomp.classical.functions]
    SurjFun_Inj.phant_axioms [def, in mathcomp.classical.functions]
    SurjFun_Inj.phant_Build [def, in mathcomp.classical.functions]
    SurjFun_Inj.SurjFun_Inj.A [var, in mathcomp.classical.functions]
    SurjFun_Inj.SurjFun_Inj.aT [var, in mathcomp.classical.functions]
    SurjFun_Inj.SurjFun_Inj.B [var, in mathcomp.classical.functions]
    SurjFun_Inj.SurjFun_Inj.f [var, in mathcomp.classical.functions]
    SurjFun_Inj.SurjFun_Inj.local_mixin_functions_isFun [var, in mathcomp.classical.functions]
    SurjFun_Inj.SurjFun_Inj.local_mixin_functions_OInv [var, in mathcomp.classical.functions]
    SurjFun_Inj.SurjFun_Inj.local_mixin_functions_OInv_CanV [var, in mathcomp.classical.functions]
    SurjFun_Inj.SurjFun_Inj.rT [var, in mathcomp.classical.functions]
    SurjFun_Inj.SurjFun_Inj_f__canonical__functions_Fun [def, in mathcomp.classical.functions]
    SurjFun_Inj.SurjFun_Inj_f__canonical__functions_OInversible [def, in mathcomp.classical.functions]
    SurjFun_Inj.SurjFun_Inj_f__canonical__functions_OInvFun [def, in mathcomp.classical.functions]
    SurjFun_Inj.SurjFun_Inj_f__canonical__functions_Surject [def, in mathcomp.classical.functions]
    SurjFun_Inj.SurjFun_Inj_f__canonical__functions_SurjFun [def, in mathcomp.classical.functions]
    SurjFunElpiOperations [mod, in mathcomp.classical.functions]
    surjfunPex [prf, in mathcomp.classical.cardinality]
    surjoinv_inj_subproof [prf, in mathcomp.classical.functions]
    surjPex [prf, in mathcomp.classical.cardinality]
    surjPfun [prf, in mathcomp.classical.functions]
    surjPfun.A [var, in mathcomp.classical.functions]
    surjPfun.aT [var, in mathcomp.classical.functions]
    surjPfun.B [var, in mathcomp.classical.functions]
    surjPfun.f [var, in mathcomp.classical.functions]
    surjPfun.ffun [var, in mathcomp.classical.functions]
    surjPfun.g [var, in mathcomp.classical.functions]
    surjPfun.rT [var, in mathcomp.classical.functions]
    surjpinv_bij [prf, in mathcomp.classical.functions]
    surjpinv_image_sub [prf, in mathcomp.classical.functions]
    surjpinv_inj [prf, in mathcomp.classical.functions]
    surjpK [prf, in mathcomp.classical.functions]
    swap [def, in mathcomp.classical.mathcomp_extra]
    swap_continuous [prf, in mathcomp.analysis.topology_theory.product_topology]
    swapK [prf, in mathcomp.classical.mathcomp_extra]
    symmetric_form [abbrev, in mathcomp.analysis.forms]
    Generated by a fork of coq2html