Commit 2023-06-29 08:26 4574002d

View on Github →

feat: add Filter.eq_or_neBot (#5230) Also add Filter.limsup_bot, Filter.liminf_bot, and golf some proofs using new lemmas.

Estimated changes

Modified Mathlib/Analysis/Complex/LocallyUniformLimit.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean

Modified Mathlib/MeasureTheory/Constructions/Polish.lean

Modified Mathlib/MeasureTheory/Covering/DensityTheorem.lean

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.eq_or_neBot

Modified Mathlib/Order/LiminfLimsup.lean

added theorem Filter.liminf_bot

added theorem Filter.limsup_bot

Modified Mathlib/Topology/Algebra/Order/LiminfLimsup.lean