'K' (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 | _ | * |
K (Definitions)
kadd [def, in mathcomp.analysis.kernel]kcomp [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.HB_unnamed_factory_160 [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.HB_unnamed_factory_162 [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.HB_unnamed_mixin_167 [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.HB_unnamed_mixin_168 [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.HB_unnamed_mixin_169 [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.HB_unnamed_mixin_170 [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.kernel_Kernel_isFinite__to__kernel_isFiniteTransition [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.kernel_Kernel_isFinite__to__kernel_isMeasureFamUub [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.kernel_Kernel_isFinite__to__kernel_isSFiniteKernel_subdef [def, in mathcomp.analysis.kernel]
KCOMP_FINITE_KERNEL.kernel_Kernel_isFinite__to__kernel_isSigmaFiniteTransitionKernel [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_FiniteTransitionKernel [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_FINITE_KERNEL.kernel_mkcomp__canonical__kernel_SigmaFiniteTransitionKernel [def, in mathcomp.analysis.kernel]
kcomp_noparam [def, in mathcomp.analysis.kernel]
KCOMP_SFINITE_KERNEL.HB_unnamed_factory_171 [def, in mathcomp.analysis.kernel]
KCOMP_SFINITE_KERNEL.HB_unnamed_factory_173 [def, in mathcomp.analysis.kernel]
KCOMP_SFINITE_KERNEL.HB_unnamed_mixin_175 [def, in mathcomp.analysis.kernel]
KCOMP_SFINITE_KERNEL.kernel_Kernel_isSFinite__to__kernel_isSFiniteKernel_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.pack_ [def, in mathcomp.analysis.kernel]
Kernel.phant_clone [def, in mathcomp.analysis.kernel]
Kernel.phant_on_ [def, in mathcomp.analysis.kernel]
kernel_finite_transition [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_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__HBNNSimple_NonNegSimpleFun [def, in mathcomp.analysis.kernel]
kernel_k_2__canonical__numfun_NonNegFun [def, in mathcomp.analysis.kernel]
kernel_k_2__canonical__simple_functions_MeasurableFun [def, in mathcomp.analysis.kernel]
kernel_kadd__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
kernel_kadd__canonical__kernel_FiniteTransitionKernel [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_kadd__canonical__kernel_SigmaFiniteTransitionKernel [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_kcomp_noparam__canonical__measure_Content [def, in mathcomp.analysis.kernel]
kernel_kcomp_noparam__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_FiniteTransitionKernel [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_SigmaFiniteTransitionKernel [def, in mathcomp.analysis.kernel]
kernel_kdirac__canonical__kernel_SubProbabilityKernel [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isFiniteTransition [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isFiniteTransition__123 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isFiniteTransition__205 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isFiniteTransition__34 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isMeasureFamUub [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isMeasureFamUub__121 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isMeasureFamUub__203 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isMeasureFamUub__32 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isSFiniteKernel_subdef [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isSFiniteKernel_subdef__127 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isSFiniteKernel_subdef__209 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isSFiniteKernel_subdef__38 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isSigmaFiniteTransitionKernel [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isSigmaFiniteTransitionKernel__125 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isSigmaFiniteTransitionKernel__207 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isFinite__to__kernel_isSigmaFiniteTransitionKernel__36 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isFiniteTransition [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isFiniteTransition__106 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isFiniteTransition__147 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isMeasureFamUub [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isMeasureFamUub__104 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isMeasureFamUub__145 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isProbabilityKernel [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isProbabilityKernel__137 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isProbabilityKernel__96 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isSFiniteKernel_subdef [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isSFiniteKernel_subdef__102 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isSFiniteKernel_subdef__143 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isSigmaFiniteTransitionKernel [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isSigmaFiniteTransitionKernel__139 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isSigmaFiniteTransitionKernel__98 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isSubProbabilityKernel [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isSubProbabilityKernel__100 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isProbability__to__kernel_isSubProbabilityKernel__141 [def, in mathcomp.analysis.kernel]
kernel_Kernel_isSubProbability__to__kernel_isFiniteTransition [def, in mathcomp.analysis.kernel]
kernel_Kernel_isSubProbability__to__kernel_isMeasureFamUub [def, in mathcomp.analysis.kernel]
kernel_Kernel_isSubProbability__to__kernel_isSFiniteKernel_subdef [def, in mathcomp.analysis.kernel]
kernel_Kernel_isSubProbability__to__kernel_isSigmaFiniteTransitionKernel [def, in mathcomp.analysis.kernel]
kernel_Kernel_isSubProbability__to__kernel_isSubProbabilityKernel [def, in mathcomp.analysis.kernel]
kernel_kernel_snd__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
kernel_kernel_snd__canonical__kernel_FiniteTransitionKernel [def, in mathcomp.analysis.kernel]
kernel_kernel_snd__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
kernel_kernel_snd__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
kernel_kernel_snd__canonical__kernel_SigmaFiniteTransitionKernel [def, in mathcomp.analysis.kernel]
kernel_kernel_snd__canonical__kernel_SubProbabilityKernel [def, in mathcomp.analysis.kernel]
kernel_knormalize__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
kernel_knormalize__canonical__kernel_FiniteTransitionKernel [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_SigmaFiniteTransitionKernel [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_FiniteTransitionKernel [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_SigmaFiniteTransitionKernel [def, in mathcomp.analysis.kernel]
kernel_kprobability__canonical__kernel_SubProbabilityKernel [def, in mathcomp.analysis.kernel]
kernel_kproduct__canonical__measure_Content [def, in mathcomp.analysis.kernel]
kernel_kproduct__canonical__measure_Measure [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_FiniteTransitionKernel [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_kzero__canonical__kernel_SigmaFiniteTransitionKernel [def, in mathcomp.analysis.kernel]
kernel_mkcomp_noparam__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
kernel_mkcomp_noparam__canonical__kernel_FiniteTransitionKernel [def, in mathcomp.analysis.kernel]
kernel_mkcomp_noparam__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
kernel_mkcomp_noparam__canonical__kernel_SFiniteKernel [def, in mathcomp.analysis.kernel]
kernel_mkcomp_noparam__canonical__kernel_SigmaFiniteTransitionKernel [def, in mathcomp.analysis.kernel]
kernel_mkcomp_noparam__canonical__kernel_SubProbabilityKernel [def, in mathcomp.analysis.kernel]
kernel_mkproduct__canonical__kernel_Kernel [def, in mathcomp.analysis.kernel]
kernel_mkproduct__canonical__kernel_SigmaFiniteTransitionKernel [def, in mathcomp.analysis.kernel]
kernel_s__canonical__kernel_FiniteKernel [def, in mathcomp.analysis.kernel]
kernel_s__canonical__kernel_FiniteTransitionKernel [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]
kernel_s__canonical__kernel_SigmaFiniteTransitionKernel [def, in mathcomp.analysis.kernel]
kernel_sigma_finite [def, in mathcomp.analysis.kernel]
kernel_snd [def, in mathcomp.analysis.kernel]
kfcomp [def, in mathcomp.analysis.kernel]
knormalize [def, in mathcomp.analysis.kernel]
KnownSign.nullity_bool [def, in mathcomp.reals.signed]
KnownSign.nz_of_bool [def, in mathcomp.reals.signed]
KnownSign.wider_nullity [def, in mathcomp.reals.signed]
KnownSign.wider_real [def, in mathcomp.reals.signed]
KnownSign.wider_reality [def, in mathcomp.reals.signed]
KnownSign.wider_sign [def, in mathcomp.reals.signed]
kolmogorov_space [def, in mathcomp.analysis.topology_theory.separation_axioms]
kprobability [def, in mathcomp.analysis.kernel]
kproduct [def, in mathcomp.analysis.kernel]
kproduct_snd [def, in mathcomp.analysis.kernel]
kseries [def, in mathcomp.analysis.kernel]
kzero [def, in mathcomp.analysis.kernel]