Commit 2024-10-05 09:45 f5188d97

refactor: Make the sigma-algebra in Kernel.comap implicit (#17299) ... rather than a typeclass argument. This is required to avoid making Gibbs measures and Markov chains an absolute pain to talk about. Indeed, in those two contexts, there is one "canonical" sigma-algebra along with many sigma-subalgebras of it, indexed by time or space respectively. There might be a missing Lean feature here. To be investigated further. From GibbsMeasure