1.16. ForMathlib.Probability.Kernel.Composition.MapComap🔗

Lemmas about map and comap of Markov kernels

Module LeanMachineLearning.ForMathlib.Probability.Kernel.Composition.MapComap contains 4 exposed declarations.

• ProbabilityTheory.Kernel.prodMkLeft_injLemma · 0 deps
• ProbabilityTheory.Kernel.prodMkRight_injLemma · 0 deps
• ProbabilityTheory.Kernel.prodMkLeft_deterministicLemma · 0 deps
• ProbabilityTheory.Kernel.prodMkRight_deterministicLemma · 0 deps