Theorem MeasureTheory.tendstoUniformlyOn_of_ae_tendsto'

Modification history

2026-10-13 16:28

Mathlib/MeasureTheory/Function/Egorov.lean

refactor(MeasureTheory/Function): generalize Egorov's theorem (#44804) …

Modified MeasureTheory.tendstoUniformlyOn_of_ae_tendsto'View on Github →

2023-06-04 05:44

Mathlib/MeasureTheory/Function/Egorov.lean

style: recover `Is` of `Foo` which is ported from `is_foo` (#4639) …

Modified MeasureTheory.tendstoUniformlyOn_of_ae_tendsto'View on Github →

2023-05-25 11:48

Mathlib/MeasureTheory/Function/Egorov.lean

feat: port MeasureTheory.Function.Egorov (#4333)

Added MeasureTheory.tendstoUniformlyOn_of_ae_tendsto'View on Github →