Theorem ProbabilityTheory.IsFiniteKernel.bound_eq_zero_of_isEmpty'

Modification history

2025-09-13 15:32

Mathlib/Probability/Kernel/Defs.lean

chore(Probability): rename IsFiniteKernel.bound to Kernel.bound (#29613) …

Deleted ProbabilityTheory.IsFiniteKernel.bound_eq_zero_of_isEmpty'View on Github →

2025-09-12 14:29

Mathlib/Probability/Kernel/Defs.lean

feat(Probability/Kernel): change the def of `IsFiniteKernel.bound` to make it more informative (#29137) …

Added ProbabilityTheory.IsFiniteKernel.bound_eq_zero_of_isEmpty'View on Github →