Mathlib Changelog
v4
Changelog
About
Github
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