Theorem ProbabilityTheory.condDistrib_self

Modification history

2026-08-26 08:21
Mathlib/Probability/Kernel/CondDistrib.lean
refactor: change the default value of `Measure.map` to a Dirac mass (#42322) …
Modified ProbabilityTheory.condDistrib_selfView on Github →
2025-10-01 13:25
Mathlib/Probability/Kernel/CondDistrib.lean
feat(Probability): `condDistrib` lemmas (#29555) …
Added ProbabilityTheory.condDistrib_selfView on Github →