Def ProbabilityTheory.countableFiltration

Modification history

2026-07-24 07:15

Mathlib/Probability/Process/PartitionFiltration.lean

chore: add missing `noncomputable` (#41446) …

Deleted ProbabilityTheory.countableFiltration View on Github →

2024-03-13 15:40

Mathlib/Probability/Process/PartitionFiltration.lean

feat: countable filtration in a countably generated measurable space (#10945) …

Added ProbabilityTheory.countableFiltration View on Github →