'S' (Definitions)

Files

G

J

V

Y

Z

_

*

Definitions

_

*

Lemmas

*

Abbreviations

J

K

Y

Z

_

*

Global Index

S (Definitions)

s_finite [def, in mathcomp.analysis.measure]
same_prefix [def, in mathcomp.classical.classical_orders]
scale_ball [def, in mathcomp.analysis.normedtype]
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]
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_theory.topology_structure]
self_sub [def, in mathcomp.analysis.normedtype]
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.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.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]
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]
separate_points_from_closed [def, in mathcomp.analysis.function_spaces]
separated [def, in mathcomp.analysis.topology_theory.connected]
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]
seqD [def, in mathcomp.analysis.sequences]
seqDU [def, in mathcomp.analysis.sequences]
sequence [def, in mathcomp.analysis.sequences]
sequences_expR__canonical__lebesgue_integral_MeasurableFun [def, in mathcomp.analysis.lebesgue_integral]
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_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_itv_infty_set0 [def, in mathcomp.classical.set_interval]
set_itvE [def, in mathcomp.classical.set_interval]
set_nbhs [def, in mathcomp.analysis.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]
setDI_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]
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.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.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]
setring [def, 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.decomp [def, in mathcomp.analysis.measure]
SetRing.display [def, 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.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.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]
SetRing_measure__canonical__measure_Measure [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.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.pack_ [def, in mathcomp.analysis.kernel]
SFiniteKernel.phant_clone [def, in mathcomp.analysis.kernel]
SFiniteKernel.phant_on_ [def, in mathcomp.analysis.kernel]
SFiniteKernel_isFinite.identity_builder [def, in mathcomp.analysis.kernel]
SFiniteKernel_isFinite.phant_axioms [def, in mathcomp.analysis.kernel]
SFiniteKernel_isFinite.phant_Build [def, in mathcomp.analysis.kernel]
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.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]
sfun_key [def, in mathcomp.analysis.lebesgue_integral]
sfun_keyed [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]
shift [def, in mathcomp.analysis.normedtype]
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.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.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.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.pack_ [def, in mathcomp.analysis.measure]
SigmaFiniteMeasure.phant_clone [def, in mathcomp.analysis.measure]
SigmaFiniteMeasure.phant_on_ [def, 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.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]
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]
sigR [def, in mathcomp.classical.functions]
SigSub [def, in mathcomp.classical.classical_sets]
sigT_fun [def, in mathcomp.classical.mathcomp_extra]
sigT_nbhs [def, in mathcomp.analysis.topology_theory.sigT_topology]
sigT_of_setX [def, in mathcomp.analysis.topology_theory.subtype_topology]
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]
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_unlock_subterm [def, in mathcomp.analysis.trigo]
singletons [def, in mathcomp.analysis.function_spaces]
sintegral [def, in mathcomp.analysis.lebesgue_integral]
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]
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_ [def, in mathcomp.classical.functions]
split_ent [def, in mathcomp.analysis.topology_theory.uniform_structure]
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.pack_ [def, in mathcomp.classical.functions]
SplitBij.phant_clone [def, in mathcomp.classical.functions]
SplitBij.phant_on_ [def, 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.pack_ [def, in mathcomp.classical.functions]
SplitInj.phant_clone [def, in mathcomp.classical.functions]
SplitInj.phant_on_ [def, 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.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]
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]
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.pack_ [def, in mathcomp.classical.functions]
SplitSurj.phant_clone [def, in mathcomp.classical.functions]
SplitSurj.phant_on_ [def, 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.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]
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]
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]
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]
start_with [def, in mathcomp.classical.classical_orders]
strace [def, in mathcomp.analysis.measure]
strictly_dominated_by [def, in mathcomp.analysis.normedtype]
sub_klipschitz [def, in mathcomp.analysis.normedtype]
sub_lipschitz [def, in mathcomp.analysis.normedtype]
subadditive [def, in mathcomp.analysis.measure]
subfun [def, in mathcomp.classical.functions]
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.pack_ [def, in mathcomp.analysis.measure]
SubProbability.phant_clone [def, in mathcomp.analysis.measure]
SubProbability.phant_on_ [def, in mathcomp.analysis.measure]
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]
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.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]
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]
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]
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.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]
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]
sups [def, in mathcomp.analysis.sequences]
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.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.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.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]
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]
swap [def, in mathcomp.classical.mathcomp_extra]