K (Definitions)
kadd [def, in mathcomp.analysis.kernel]
kcomp [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.HB_unnamed_factory_149 [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.HB_unnamed_factory_151 [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.HB_unnamed_mixin_154 [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.HB_unnamed_mixin_155 [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.kernel_Kernel_isFinite__to__kernel_Kernel_isSFinite_subdef [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.kernel_Kernel_isFinite__to__kernel_SFiniteKernel_isFinite [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.kernel_mkcomp__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.kernel_mkcomp__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.kernel_mkcomp__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
KCOMP_SFINITE_KERNEL.HB_unnamed_factory_156 [def, in mathcomp.analysis.kernel]
KCOMP_SFINITE_KERNEL.HB_unnamed_factory_158 [def, in mathcomp.analysis.kernel]
KCOMP_SFINITE_KERNEL.HB_unnamed_mixin_160 [def, in mathcomp.analysis.kernel]
KCOMP_SFINITE_KERNEL.kernel_Kernel_isSFinite__to__kernel_Kernel_isSFinite_subdef [def, in mathcomp.analysis.kernel]
KCOMP_SFINITE_KERNEL.kernel_mkcomp__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
KCOMP_SFINITE_KERNEL.kernel_mkcomp__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
kdirac [def, in mathcomp.analysis.kernel]
Kernel.EtaAndMixinExports.HB_unnamed_factory_2 [def, in mathcomp.analysis.kernel]
Kernel.EtaAndMixinExports.HB_unnamed_mixin_4 [def, in mathcomp.analysis.kernel]
Kernel.EtaAndMixinExports.kernel_Kernel__to__kernel_isKernel [def, in mathcomp.analysis.kernel]
Kernel.EtaAndMixinExports.structures_eta__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
Kernel.pack_ [def, in mathcomp.analysis.kernel]
Kernel.phant_clone [def, in mathcomp.analysis.kernel]
Kernel.phant_on_ [def, in mathcomp.analysis.kernel]
Kernel_isFinite.Kernel_isFinite_k__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
Kernel_isFinite.phant_axioms [def, in mathcomp.analysis.kernel]
Kernel_isFinite.phant_Build [def, in mathcomp.analysis.kernel]
Kernel_isProbability.Kernel_isProbability_k__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
Kernel_isProbability.phant_axioms [def, in mathcomp.analysis.kernel]
Kernel_isProbability.phant_Build [def, in mathcomp.analysis.kernel]
Kernel_isSFinite.Kernel_isSFinite_k__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
Kernel_isSFinite.phant_axioms [def, in mathcomp.analysis.kernel]
Kernel_isSFinite.phant_Build [def, in mathcomp.analysis.kernel]
Kernel_isSFinite_subdef.identity_builder [def, in mathcomp.analysis.kernel]
Kernel_isSFinite_subdef.phant_axioms [def, in mathcomp.analysis.kernel]
Kernel_isSFinite_subdef.phant_Build [def, in mathcomp.analysis.kernel]
Kernel_isSubProbability.Kernel_isSubProbability_k__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
Kernel_isSubProbability.phant_axioms [def, in mathcomp.analysis.kernel]
Kernel_isSubProbability.phant_Build [def, in mathcomp.analysis.kernel]
kernel_k_2__canonical__cardinality_FImFun [def, in mathcomp.analysis.kernel]
kernel_k_2__canonical__lebesgue_integral_MeasurableFun [def, in mathcomp.analysis.kernel]
kernel_k_2__canonical__lebesgue_integral_NonNegSimpleFun [def, in mathcomp.analysis.kernel]
kernel_k_2__canonical__lebesgue_integral_SimpleFun [def, in mathcomp.analysis.kernel]
kernel_k_2__canonical__numfun_NonNegFun [def, in mathcomp.analysis.kernel]
kernel_kadd__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
kernel_kadd__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
kernel_kadd__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
kernel_kcomp__canonical__measure_Content [def, in mathcomp.analysis.kernel]
kernel_kcomp__canonical__measure_Measure [def, in mathcomp.analysis.kernel]
kernel_kD__canonical__measure_Content [def, in mathcomp.analysis.kernel]
kernel_kD__canonical__measure_Measure [def, in mathcomp.analysis.kernel]
kernel_kdirac__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
kernel_kdirac__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
kernel_kdirac__canonical__kernel_ProbabilityKernel [def, in mathcomp.analysis.kernel]
kernel_kdirac__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
kernel_kdirac__canonical__kernel_SubProbabilityKernel [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_Kernel_isSFinite_subdef [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_Kernel_isSFinite_subdef__126 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_Kernel_isSFinite_subdef__43 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_SFiniteKernel_isFinite [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_SFiniteKernel_isFinite__124 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_SFiniteKernel_isFinite__41 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_FiniteKernel_isSubProbability [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_FiniteKernel_isSubProbability__111 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_FiniteKernel_isSubProbability__138 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_Kernel_isSFinite_subdef [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_Kernel_isSFinite_subdef__109 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_Kernel_isSFinite_subdef__136 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_SFiniteKernel_isFinite [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_SFiniteKernel_isFinite__107 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_SFiniteKernel_isFinite__134 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_SubProbability_isProbability [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_SubProbability_isProbability__105 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_SubProbability_isProbability__132 [def, in mathcomp.analysis.kernel]
kernel_knormalize__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
kernel_knormalize__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
kernel_knormalize__canonical__kernel_ProbabilityKernel [def, in mathcomp.analysis.kernel]
kernel_knormalize__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
kernel_knormalize__canonical__kernel_SubProbabilityKernel [def, in mathcomp.analysis.kernel]
kernel_kprobability__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
kernel_kprobability__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
kernel_kprobability__canonical__kernel_ProbabilityKernel [def, in mathcomp.analysis.kernel]
kernel_kprobability__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
kernel_kprobability__canonical__kernel_SubProbabilityKernel [def, in mathcomp.analysis.kernel]
kernel_kseries__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
kernel_kseries__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
kernel_kzero__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
kernel_kzero__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
kernel_kzero__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
kernel_s__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
kernel_s__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
kernel_s__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
knormalize [def, in mathcomp.analysis.kernel]
KnownSign.nullity_bool [def, in mathcomp.analysis.signed]
KnownSign.nz_of_bool [def, in mathcomp.analysis.signed]
KnownSign.wider_nullity [def, in mathcomp.analysis.signed]
KnownSign.wider_real [def, in mathcomp.analysis.signed]
KnownSign.wider_reality [def, in mathcomp.analysis.signed]
KnownSign.wider_sign [def, in mathcomp.analysis.signed]
kolmogorov_space [def, in mathcomp.analysis.topology]
kprobability [def, in mathcomp.analysis.kernel]
kseries [def, in mathcomp.analysis.kernel]
kzero [def, in mathcomp.analysis.kernel]