Commit 2020-07-28 17:35 9f51e336

View on Github →

feat(measure_theory/measurable_space): introduce filter.is_measurably_generated (#3594) Sometimes I want to extract an is_measurable witness of a filter.eventually statement.

Estimated changes

Modified src/measure_theory/borel_space.lean

added theorem is_measurable.nhds_within_is_measurably_generated

Modified src/measure_theory/measurable_space.lean

added theorem filter.eventually.exists_measurable_mem

added theorem filter.principal_is_measurably_generated_iff

Modified src/measure_theory/measure_space.lean