mathlib
c5b46faa - feat(measure_theory/measurable_space): add `measurable_of_countable` (#17266)

Commit

3 years ago

feat(measure_theory/measurable_space): add `measurable_of_countable` (#17266) Every function from a countable type with measurable singletons is measurable.

Author

RemyDegenne

Parents

65ee8572

mathlib c5b46faa - feat(measure_theory/measurable_space): add `measurable_of_countable` (#17266)

mathlib
c5b46faa - feat(measure_theory/measurable_space): add `measurable_of_countable` (#17266)