Commit 2022-12-22 07:41 207cfac9

View on Github →

feat(measure_theory/measurable_space) add measurable Schroeder-Bernstein (#17988) Add a version of the Schroeder-Bernstein theorem for measurable spaces, embeddings, and equivalences.

Estimated changes

Modified src/measure_theory/measurable_space.lean

modified theorem measurable_embedding.of_measurable_inverse

added def measurable_embedding.schroeder_bernstein

added def measurable_equiv.sum_compl