S (Definitions)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Notations |
S (Definitions)
s_finite [def, in mathcomp.analysis.measure]same_prefix [def, in mathcomp.classical.classical_orders]
scale_ball [def, in mathcomp.analysis.normedtype_theory.vitali_lemma]
scale_continuous [def, in mathcomp.analysis.tvs]
scale_fimfun [def, in mathcomp.analysis.numfun]
scale_littleo [def, in mathcomp.analysis.landau]
scale_mfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
scale_nnsfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
scale_sfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
scale_unif_continuous [def, in mathcomp.analysis.tvs]
sdrop [def, in mathcomp.analysis.sequences]
second_countable [def, in mathcomp.analysis.topology_theory.topology_structure]
self_sub [def, in mathcomp.analysis.normedtype_theory.normed_module]
selfFiltered.identity_builder [def, in mathcomp.classical.filter]
selfFiltered.phant_axioms [def, in mathcomp.classical.filter]
selfFiltered.phant_Build [def, in mathcomp.classical.filter]
semi_additive [def, in mathcomp.analysis.measure]
semi_additive2 [def, 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]
SemiRingOfSets.pack_ [def, in mathcomp.analysis.measure]
SemiRingOfSets.phant_clone [def, in mathcomp.analysis.measure]
SemiRingOfSets.phant_on_ [def, in mathcomp.analysis.measure]
SemiRingOfSets_isRingOfSets.identity_builder [def, in mathcomp.analysis.measure]
SemiRingOfSets_isRingOfSets.phant_axioms [def, in mathcomp.analysis.measure]
SemiRingOfSets_isRingOfSets.phant_Build [def, in mathcomp.analysis.measure]
separate_points_from_closed [def, in mathcomp.analysis.function_spaces]
separated [def, in mathcomp.analysis.topology_theory.connected]
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_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_theory.separation_axioms]
set_predType [def, in mathcomp.classical.classical_sets]
set_surj [def, in mathcomp.classical.functions]
set_system [def, in mathcomp.classical.filter]
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]
seteqfun [def, in mathcomp.classical.functions]
setI [def, in mathcomp.classical.classical_sets]
setI_closed [def, in mathcomp.analysis.measure]
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.type [def, in mathcomp.analysis.measure]
setSD_closed [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_closed [def, in mathcomp.analysis.measure]
setX [def, in mathcomp.classical.classical_sets]
setX_of_sigT [def, in mathcomp.analysis.topology_theory.subtype_topology]
setXL [def, in mathcomp.classical.classical_sets]
setXR [def, in mathcomp.classical.classical_sets]
setY [def, in mathcomp.classical.classical_sets]
setY_closed [def, in mathcomp.analysis.measure]
sfinite_kernel_subdef [def, in mathcomp.analysis.kernel]
sfinite_measure [def, in mathcomp.analysis.measure]
sfinite_measure_seq [def, in mathcomp.analysis.measure]
SFiniteKernel.pack_ [def, in mathcomp.analysis.kernel]
SFiniteKernel.phant_clone [def, in mathcomp.analysis.kernel]
SFiniteKernel.phant_on_ [def, in mathcomp.analysis.kernel]
SFiniteMeasure.pack_ [def, in mathcomp.analysis.measure]
SFiniteMeasure.phant_clone [def, in mathcomp.analysis.measure]
SFiniteMeasure.phant_on_ [def, in mathcomp.analysis.measure]
sfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
sfun_key [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
sfun_keyed [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
sfun_Sub [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
shift [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
sigL [def, in mathcomp.classical.functions]
sigL_arrow [def, in mathcomp.analysis.function_spaces]
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_finiteT [def, in mathcomp.analysis.measure]
sigma_ring [def, in mathcomp.analysis.measure]
sigma_subadditive [def, 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]
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.pack_ [def, in mathcomp.analysis.measure]
SigmaFiniteMeasure.phant_clone [def, in mathcomp.analysis.measure]
SigmaFiniteMeasure.phant_on_ [def, in mathcomp.analysis.measure]
SigmaFiniteTransitionKernel.pack_ [def, in mathcomp.analysis.kernel]
SigmaFiniteTransitionKernel.phant_clone [def, in mathcomp.analysis.kernel]
SigmaFiniteTransitionKernel.phant_on_ [def, in mathcomp.analysis.kernel]
SigmaRing.pack_ [def, in mathcomp.analysis.measure]
SigmaRing.phant_clone [def, in mathcomp.analysis.measure]
SigmaRing.phant_on_ [def, in mathcomp.analysis.measure]
Signed.Exports.nonneg [def, 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.reality_cond [def, in mathcomp.reals.signed]
sigR [def, in mathcomp.classical.functions]
SigSub [def, in mathcomp.classical.classical_sets]
sigT_fun [def, in mathcomp.classical.unstable]
sigT_nbhs [def, in mathcomp.analysis.topology_theory.sigT_topology]
sigT_of_setX [def, in mathcomp.analysis.topology_theory.subtype_topology]
sin.body [def, in mathcomp.analysis.trigo]
sin.unlock [def, in mathcomp.analysis.trigo]
sin_coeff [def, in mathcomp.analysis.trigo]
sin_coeff' [def, in mathcomp.analysis.trigo]
sin_inum [def, in mathcomp.analysis.trigo]
sin_unlock_subterm [def, in mathcomp.analysis.trigo]
singletons [def, in mathcomp.analysis.function_spaces]
sintegral [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
small_ent_sub [def, in mathcomp.analysis.function_spaces]
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_theory.uniform_structure]
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.pack_ [def, in mathcomp.classical.functions]
SplitBij.phant_clone [def, in mathcomp.classical.functions]
SplitBij.phant_on_ [def, in mathcomp.classical.functions]
SplitInj.Exports.join_functions_SplitInj_between_functions_Inject_and_functions_Inversible [def, 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]
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.pack_ [def, in mathcomp.classical.functions]
SplitInjFun.phant_clone [def, in mathcomp.classical.functions]
SplitInjFun.phant_on_ [def, in mathcomp.classical.functions]
SplitInjFun_CanV.phant_axioms [def, in mathcomp.classical.functions]
SplitInjFun_CanV.phant_Build [def, in mathcomp.classical.functions]
SplitSurj.Exports.join_functions_SplitSurj_between_functions_Inversible_and_functions_Surject [def, 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]
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.pack_ [def, in mathcomp.classical.functions]
SplitSurjFun.phant_clone [def, in mathcomp.classical.functions]
SplitSurjFun.phant_on_ [def, in mathcomp.classical.functions]
SplitSurjFun_Inj.phant_axioms [def, in mathcomp.classical.functions]
SplitSurjFun_Inj.phant_Build [def, in mathcomp.classical.functions]
sprob_kernel [def, in mathcomp.analysis.kernel]
sprobability_setT [def, in mathcomp.analysis.measure]
sqrt_nonzero_subdef [def, in mathcomp.reals.signed]
sqrt_snum [def, in mathcomp.reals.signed]
sqrtC_reality_subdef [def, in mathcomp.reals.signed]
sqrtC_snum [def, in mathcomp.reals.signed]
sqrte [def, in mathcomp.reals.constructive_ereal]
ssquash [def, in mathcomp.classical.functions]
start_with [def, in mathcomp.classical.classical_orders]
strace [def, in mathcomp.analysis.measure]
Streicher_K_ [def, in mathcomp.classical.internal_Eqdep_dec]
Streicher_K_on_ [def, in mathcomp.classical.internal_Eqdep_dec]
strictly_dominated_by [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
subadditive [def, in mathcomp.analysis.measure]
subfun [def, in mathcomp.classical.functions]
SubProbability.pack_ [def, in mathcomp.analysis.measure]
SubProbability.phant_clone [def, in mathcomp.analysis.measure]
SubProbability.phant_on_ [def, in mathcomp.analysis.measure]
SubProbabilityKernel.pack_ [def, in mathcomp.analysis.kernel]
SubProbabilityKernel.phant_clone [def, in mathcomp.analysis.kernel]
SubProbabilityKernel.phant_on_ [def, in mathcomp.analysis.kernel]
subset [def, in mathcomp.classical.classical_sets]
subset_filter [def, in mathcomp.classical.filter]
subset_sigma_subadditive [def, in mathcomp.analysis.measure]
subsetCW [def, in mathcomp.classical.classical_sets]
subspace [def, in mathcomp.analysis.topology_theory.subspace_topology]
subspace_ball [def, in mathcomp.analysis.topology_theory.subspace_topology]
subspace_ent [def, in mathcomp.analysis.topology_theory.subspace_topology]
succn_snum [def, in mathcomp.reals.signed]
sum [def, in mathcomp.experimental_reals.realsum]
sum [def, in mathcomp.analysis.showcase.summability]
sum_nnsfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
summable [def, in mathcomp.experimental_reals.realsum]
summable [def, in mathcomp.analysis.showcase.summability]
summable [def, in mathcomp.analysis.esum]
sup [def, in mathcomp.reals.reals]
sup_adherent_subdef [def, in mathcomp.reals.reals]
sup_ent [def, in mathcomp.analysis.topology_theory.supremum_topology]
sup_pseudometric [def, in mathcomp.analysis.topology_theory.separation_axioms]
sup_subbase [def, in mathcomp.analysis.topology_theory.supremum_topology]
sup_topology [def, in mathcomp.analysis.topology_theory.supremum_topology]
sup_upper_bound_subdef [def, in mathcomp.reals.reals]
supremum [def, in mathcomp.classical.classical_sets]
supremums [def, in mathcomp.classical.classical_sets]
sups [def, in mathcomp.analysis.sequences]
Surject.pack_ [def, in mathcomp.classical.functions]
Surject.phant_clone [def, in mathcomp.classical.functions]
Surject.phant_on_ [def, in mathcomp.classical.functions]
surjection_of_surj [def, in mathcomp.classical.functions]
surjective_ocanV [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.pack_ [def, in mathcomp.classical.functions]
SurjFun.phant_clone [def, in mathcomp.classical.functions]
SurjFun.phant_on_ [def, in mathcomp.classical.functions]
SurjFun_Inj.phant_axioms [def, in mathcomp.classical.functions]
SurjFun_Inj.phant_Build [def, in mathcomp.classical.functions]
swap [def, in mathcomp.classical.unstable]