Theorem MeasureTheory.StronglyMeasurable.limUnder

Modification history

2026-03-18 10:19
Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean
chore(Topology): rename lim -> Filter.lim and limUnder -> Filter.limUnder, and make a lemma protected (#36522) …
Deleted MeasureTheory.StronglyMeasurable.limUnderView on Github →
2025-03-24 16:18
Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean
feat: if `g` is measurable wrt to the pullback by `f` then `g` is a measurable function of `f` (#22743) …
Added MeasureTheory.StronglyMeasurable.limUnderView on Github →