Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
measure_theory.egorov.Union_not_convergent_seq_measurable_set
Modification history
2022-01-13 16:52
src/measure_theory/function/uniform_integrable.lean
feat(measure_theory/function/uniform_integrable): Egorov's theorem (#11328) …
Added
measure_theory.egorov.Union_not_convergent_seq_measurable_set
View on Github →