LeanMachineLearning

4.13. Tactic.KernelHom.Kernel.Hom🔗

Kernel morphisms

This file defines the transformation between categorical morphisms in SFinKer and kernel objects.

Main declarations

  • fromHom: transforms a categorical morphism in SFinKer to a Kernel.

  • hom: transforms a Kernel to a categorical morphism in SFinKer.

Module LeanMachineLearning.Tactic.KernelHom.Kernel.Hom contains 21 exposed declarations.