Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.eventually.exists_measurable_mem_of_lift'

Modification history

2022-04-24 20:37
src/measure_theory/measurable_space.lean
refactor(*): migrate from `filter.lift' _ powerset` to `filter.small_sets` (#13673)
Deleted filter.eventually.exists_measurable_mem_of_lift'View on Github →
2021-01-10 19:12
src/measure_theory/measurable_space.lean
chore(measure_theory/set_integral): use weaker assumptions here and there (#5647) …
Added filter.eventually.exists_measurable_mem_of_lift'View on Github →