Commit 2023-05-06 08:46 3cef175e

View on Github →

chore: forward port leanprover-community/mathlib#18910 (#3814)

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace.lean

deleted theorem MeasurableSpace.measurable_injection_cantor_of_countablyGenerated

added theorem MeasurableSpace.measurable_injection_nat_bool_of_countablyGenerated

Modified Mathlib/Topology/Perfect.lean