mathlib3

63decdb8 - feat(probability/kernel/basic): add `kernel.comap_right` and `kernel.piecewise` (#18917)

feat(probability/kernel/basic): add `kernel.comap_right` and `kernel.piecewise` (#18917) Also put `is_s_finite_kernel` in the same namespace as the other classes of kernels and add `iff` variants of the ext lemmas.