Structures · Analysis
ProbabilityTheory.IsDeterministic
A kernel is deterministic if copying then applying the kernel to the two copies is the same as first applying the kernel then copying.
- Defined in
- Mathlib.Probability.Kernel.Deterministic
- Shape
- One type argument · adds parallelComp_self_comp_copy'
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- SFinKer.carrier
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by7
- ProbabilityTheory.Kernel.parallelComp_self_comp_copy
- ProbabilityTheory.IsDeterministic.parallelComp_self_comp_copy'
- ProbabilityTheory.Kernel.IsDeterministic.exists_eq_deterministic
- SFinKer.deterministic_deterministic
- ProbabilityTheory.Kernel.instIsZeroOneMeasureCoeMeasureOfIsFiniteKernelOfIsDeterministic
- instDeterministicStochMkWideSubcategorySFinKerStochHomMkOfIsDeterministicCarrierObj
- ProbabilityTheory.Kernel.comp_parallelComp_comp_copy
Ancestors0
No ancestors.