Commit 2023-04-27 21:26 77870e4b

View on Github →

chore: forward port leanprover-community/mathlib#18864 (#3687) Forward port changes from leanprover-community/mathlib#18864 to Topology/Perfect.lean and MeasureTheory/MeasurableSpace.lean

Estimated changes

Modified Mathlib/MeasureTheory/MeasurableSpace.lean

added theorem MeasurableSpace.measurable_injection_cantor_of_countablyGenerated

added theorem measurable_to_bool

added theorem measurable_to_countable'

Modified Mathlib/Topology/Perfect.lean

added theorem IsClosed.exists_nat_bool_injection_of_not_countable