S (Definitions)
salgebraType [def, in mathcomp.analysis.measure]
salgebraType_choiceType [def, in mathcomp.analysis.measure]
salgebraType_eqType [def, in mathcomp.analysis.measure]
salgebraType_ptType [def, in mathcomp.analysis.measure]
scale_ball [def, in mathcomp.analysis.normedtype]
scale_fimfun [def, in mathcomp.analysis.numfun]
scale_littleo [def, 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]
sdrop [def, in mathcomp.analysis.sequences]
second_countable [def, in mathcomp.analysis.topology]
self_sub [def, in mathcomp.analysis.normedtype]
semi_additive [def, in mathcomp.analysis.measure]
semi_additive2 [def, in mathcomp.analysis.measure]
semi_setD_closed [def, in mathcomp.analysis.measure]
semi_sigma_additive [def, in mathcomp.analysis.measure]
semiRingOfSets_choiceType [def, in mathcomp.analysis.measure]
semiRingOfSets_eqType [def, in mathcomp.analysis.measure]
semiRingOfSets_ptType [def, in mathcomp.analysis.measure]
separate_points_from_closed [def, in mathcomp.analysis.topology]
separated [def, in mathcomp.analysis.topology]
seqD [def, in mathcomp.analysis.sequences]
seqDU [def, in mathcomp.analysis.sequences]
sequence [def, in mathcomp.analysis.sequences]
series [def, in mathcomp.analysis.sequences]
sesqui [def, in mathcomp.analysis.forms]
sesqui_keyed [def, in mathcomp.analysis.forms]
set [def, in mathcomp.classical.classical_sets]
set0 [def, in mathcomp.classical.classical_sets]
set1 [def, in mathcomp.classical.classical_sets]
set_bij [def, in mathcomp.classical.functions]
set_bij_bijfun [def, in mathcomp.classical.functions]
set_filter_source [def, in mathcomp.analysis.topology]
set_fun [def, in mathcomp.classical.functions]
set_inj [def, in mathcomp.classical.functions]
set_itv_infty_set0 [def, in mathcomp.classical.set_interval]
set_itvE [def, in mathcomp.classical.set_interval]
set_nbhs [def, in mathcomp.analysis.topology]
set_predType [def, in mathcomp.classical.classical_sets]
set_surj [def, in mathcomp.classical.functions]
set_type [def, in mathcomp.classical.classical_sets]
set_val [def, in mathcomp.classical.functions]
setC [def, in mathcomp.classical.classical_sets]
setC_closed [def, in mathcomp.analysis.measure]
setC_inj [def, in mathcomp.classical.classical_sets]
setD [def, in mathcomp.classical.classical_sets]
setD_closed [def, in mathcomp.analysis.measure]
setDI_closed [def, in mathcomp.analysis.measure]
seteqfun [def, in mathcomp.classical.functions]
setI [def, in mathcomp.classical.classical_sets]
setI_add_monoid [def, in mathcomp.classical.classical_sets]
setI_closed [def, in mathcomp.analysis.measure]
setI_comoid [def, in mathcomp.classical.classical_sets]
setI_monoid [def, in mathcomp.classical.classical_sets]
setI_mul_monoid [def, in mathcomp.classical.classical_sets]
setM [def, in mathcomp.classical.classical_sets]
setML [def, in mathcomp.classical.classical_sets]
setMR [def, in mathcomp.classical.classical_sets]
SetOrder.Internal.bDistrLatticeType [def, in mathcomp.classical.classical_sets]
SetOrder.Internal.bLatticeType [def, in mathcomp.classical.classical_sets]
SetOrder.Internal.cbDistrLatticeType [def, in mathcomp.classical.classical_sets]
SetOrder.Internal.ctbDistrLatticeType [def, in mathcomp.classical.classical_sets]
SetOrder.Internal.distrLatticeType [def, in mathcomp.classical.classical_sets]
SetOrder.Internal.latticeType [def, in mathcomp.classical.classical_sets]
SetOrder.Internal.orderMixin [def, in mathcomp.classical.classical_sets]
SetOrder.Internal.porderType [def, in mathcomp.classical.classical_sets]
SetOrder.Internal.tbDistrLatticeType [def, in mathcomp.classical.classical_sets]
SetOrder.Internal.tbLatticeType [def, in mathcomp.classical.classical_sets]
setring [def, in mathcomp.analysis.measure]
SetRing.decomp [def, in mathcomp.analysis.measure]
SetRing.display [def, in mathcomp.analysis.measure]
SetRing.measurable_fin_trivIset [def, in mathcomp.analysis.measure]
SetRing.measure [def, in mathcomp.analysis.measure]
SetRing.ring_choiceType [def, in mathcomp.analysis.measure]
SetRing.ring_eqType [def, in mathcomp.analysis.measure]
SetRing.ring_ptType [def, in mathcomp.analysis.measure]
SetRing.type [def, in mathcomp.analysis.measure]
setT [def, in mathcomp.classical.classical_sets]
setTbij [def, in mathcomp.classical.functions]
setU [def, in mathcomp.classical.classical_sets]
setU_add_monoid [def, in mathcomp.classical.classical_sets]
setU_closed [def, in mathcomp.analysis.measure]
setU_comoid [def, in mathcomp.classical.classical_sets]
setU_monoid [def, in mathcomp.classical.classical_sets]
setU_mul_monoid [def, in mathcomp.classical.classical_sets]
sfinite_measure [def, in mathcomp.analysis.measure]
sfinite_measure_seq [def, in mathcomp.analysis.measure]
sfun [def, in mathcomp.analysis.lebesgue_integral]
sfun_add [def, in mathcomp.analysis.lebesgue_integral]
sfun_comRingMixin [def, in mathcomp.analysis.lebesgue_integral]
sfun_comRingType [def, in mathcomp.analysis.lebesgue_integral]
sfun_key [def, in mathcomp.analysis.lebesgue_integral]
sfun_keyed [def, in mathcomp.analysis.lebesgue_integral]
sfun_mul [def, in mathcomp.analysis.lebesgue_integral]
sfun_ringMixin [def, in mathcomp.analysis.lebesgue_integral]
sfun_ringType [def, 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 [def, in mathcomp.analysis.lebesgue_integral]
sfun_subType [def, in mathcomp.analysis.lebesgue_integral]
sfun_zmod [def, in mathcomp.analysis.lebesgue_integral]
sfun_zmodMixin [def, in mathcomp.analysis.lebesgue_integral]
sfun_zmodType [def, in mathcomp.analysis.lebesgue_integral]
sfunchoiceMixin [def, in mathcomp.analysis.lebesgue_integral]
sfunchoiceType [def, in mathcomp.analysis.lebesgue_integral]
sfuneqMixin [def, in mathcomp.analysis.lebesgue_integral]
sfuneqType [def, in mathcomp.analysis.lebesgue_integral]
shift [def, in mathcomp.analysis.normedtype]
sigL [def, in mathcomp.classical.functions]
sigLfun [def, in mathcomp.classical.functions]
sigLR [def, in mathcomp.classical.functions]
sigma_additive [def, in mathcomp.analysis.measure]
sigma_algebra [def, in mathcomp.analysis.measure]
sigma_display [def, in mathcomp.analysis.measure]
sigma_finite [def, in mathcomp.analysis.measure]
sigma_sub_additive [def, in mathcomp.analysis.measure]
sigma_subadditive [def, in mathcomp.analysis.measure]
Signed.Exports.nonneg [def, in mathcomp.analysis.signed]
Signed.Exports.posnum [def, in mathcomp.analysis.signed]
Signed.from [def, in mathcomp.analysis.signed]
Signed.fromP [def, in mathcomp.analysis.signed]
Signed.is_real [def, in mathcomp.analysis.signed]
Signed.mk [def, in mathcomp.analysis.signed]
Signed.reality_cond [def, in mathcomp.analysis.signed]
signed_choiceMixin [def, in mathcomp.analysis.signed]
signed_choiceType [def, in mathcomp.analysis.signed]
signed_distrLatticeType [def, in mathcomp.analysis.signed]
signed_eqMixin [def, in mathcomp.analysis.signed]
signed_eqType [def, in mathcomp.analysis.signed]
signed_latticeType [def, in mathcomp.analysis.signed]
signed_orderType [def, in mathcomp.analysis.signed]
signed_porderMixin [def, in mathcomp.analysis.signed]
signed_porderType [def, in mathcomp.analysis.signed]
signed_subType [def, in mathcomp.analysis.signed]
sigR [def, in mathcomp.classical.functions]
SigSub [def, in mathcomp.classical.classical_sets]
sin [def, in mathcomp.analysis.trigo]
sin_coeff [def, in mathcomp.analysis.trigo]
sin_coeff' [def, in mathcomp.analysis.trigo]
singletons [def, in mathcomp.analysis.topology]
sintegral [def, in mathcomp.analysis.lebesgue_integral]
small_ent_sub [def, in mathcomp.analysis.topology]
smallest [def, in mathcomp.classical.classical_sets]
snd_fset [def, in mathcomp.classical.cardinality]
snd_set [def, in mathcomp.classical.classical_sets]
split_ [def, in mathcomp.classical.functions]
split_ent [def, in mathcomp.analysis.topology]
sqrt_nonzero_subdef [def, in mathcomp.analysis.signed]
sqrt_snum [def, in mathcomp.analysis.signed]
sqrtC_reality_subdef [def, in mathcomp.analysis.signed]
sqrtC_snum [def, in mathcomp.analysis.signed]
sqrte [def, in mathcomp.analysis.constructive_ereal]
ssquash [def, in mathcomp.classical.functions]
step_ball [def, in mathcomp.analysis.topology]
strace [def, in mathcomp.analysis.lebesgue_measure]
strictly_dominated_by [def, in mathcomp.analysis.normedtype]
sub_additive [def, in mathcomp.analysis.measure]
sub_klipschitz [def, in mathcomp.analysis.normedtype]
sub_lipschitz [def, in mathcomp.analysis.normedtype]
subfun [def, in mathcomp.classical.functions]
subset [def, in mathcomp.classical.classical_sets]
subset_filter [def, in mathcomp.analysis.topology]
subsetCW [def, in mathcomp.classical.classical_sets]
subspace [def, in mathcomp.analysis.topology]
subspace_ball [def, in mathcomp.analysis.topology]
subspace_ent [def, in mathcomp.analysis.topology]
subspace_filteredType [def, in mathcomp.analysis.topology]
subspace_pointedType [def, in mathcomp.analysis.topology]
subspace_pseudoMetricType [def, in mathcomp.analysis.topology]
subspace_pseudoMetricType_mixin [def, in mathcomp.analysis.topology]
subspace_topologicalMixin [def, in mathcomp.analysis.topology]
subspace_topologicalType [def, in mathcomp.analysis.topology]
subspace_uniformMixin [def, in mathcomp.analysis.topology]
subspace_uniformType [def, in mathcomp.analysis.topology]
succn_snum [def, in mathcomp.analysis.signed]
sum [def, in mathcomp.analysis.summability]
sum_nnsfun [def, in mathcomp.analysis.lebesgue_integral]
summable [def, in mathcomp.analysis.esum]
summable [def, in mathcomp.analysis.summability]
sup [def, in mathcomp.analysis.reals]
sup_ent [def, in mathcomp.analysis.topology]
sup_ent_filter [def, in mathcomp.analysis.topology]
sup_pseudoMetric_mixin [def, in mathcomp.analysis.topology]
sup_pseudoMetricType [def, in mathcomp.analysis.topology]
sup_subbase [def, in mathcomp.analysis.topology]
sup_topologicalType [def, in mathcomp.analysis.topology]
sup_topologicalTypeMixin [def, in mathcomp.analysis.topology]
sup_uniform_mixin [def, in mathcomp.analysis.topology]
sup_uniformType [def, in mathcomp.analysis.topology]
supremum [def, in mathcomp.classical.classical_sets]
supremums [def, in mathcomp.classical.classical_sets]
sups [def, in mathcomp.analysis.sequences]
surjection_of_surj [def, in mathcomp.classical.functions]
surjective_ocanV [def, in mathcomp.classical.functions]
swap [def, in mathcomp.classical.mathcomp_extra]