Theorem MeasureTheory.tendstoUniformlyOn_of_ae_tendsto'

Modification history

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 →