Commit 2024-09-03 17:59 b804674c

View on Github →

feat(MeasurableSpace): Set.ncard is measurable (#16205)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

added theorem ENat.measurable_iff

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Instances.lean

Created Mathlib/MeasureTheory/MeasurableSpace/NCard.lean

added theorem measurable_encard

added theorem measurable_ncard