Def memPartitionSet

Modification history

2026-07-24 07:15

Mathlib/Data/Set/MemPartition.lean

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

Deleted memPartitionSet View on Github →

2024-03-13 15:40

Mathlib/Data/Set/MemPartition.lean

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

Added memPartitionSet View on Github →