Mathlib v3 is deprecated. Go to Mathlib v4

Theorem filter.eventually.exists_measurable_mem_of_small_sets

Modification history

2022-04-24 20:37

src/measure_theory/measurable_space.lean

refactor(*): migrate from `filter.lift' _ powerset` to `filter.small_sets` (#13673)

Added filter.eventually.exists_measurable_mem_of_small_sets View on Github →