Theorem ProbabilityTheory.Kernel.isIrreducible_of_le_measure

Modification history

2025-11-29 08:58
Mathlib/Probability/Kernel/Irreducible.lean
feat(Probability/Kernel): \phi-irreducibility of kernels (#29734) …
Added ProbabilityTheory.Kernel.isIrreducible_of_le_measureView on Github →