4.1. Tactic.EqLift.ForMathlib.Kernel🔗

Kernel utilities

This file provides helper lemmas for working with kernels.

Main declarations

• comap_parallelComp_comap: the comap of a parallel composition is the parallel composition of the comaps.

• map_parallelComp_map: the map of a parallel composition is the parallel composition of the maps.

Module LeanMachineLearning.Tactic.EqLift.ForMathlib.Kernel contains 3 exposed declarations.

• ProbabilityTheory.Kernel.comap_parallelComp_comapLemma · 0 deps
• ProbabilityTheory.Kernel.map_parallelComp_mapLemma · 0 deps
• ProbabilityTheory.Kernel.instIsSFiniteKernelOfIsDeterministic_leanMachineLearningInstance · 0 deps