Commit 2024-09-17 15:51 eb17e512

View on Github →

chore: remove unnecessary NeBot assumptions (#16847) I analysed all the use of NeBot assumptions (that a filter needs to be non-empty). I found 10 lemmas where this assumption was unnecessary, and removed it (with some modification of the proofs when necessary). When possible, I simplified the proofs which use those lemmas. Unrelated: I cleaned up some lemmas I encountered which had universal quantifiers/chains of implications in their conclusions, using additional assumptions instead.

Estimated changes

modified theorem limsInf_nhds
modified theorem limsSup_eq_of_le_nhds
modified theorem limsup_const_sub
modified theorem limsup_sub_const
modified theorem ENNReal.liminf_const_sub
modified theorem ENNReal.limsup_const_sub
modified theorem ENNReal.limsup_sub_const
modified theorem IsGLB.isLUB_of_tendsto
modified theorem IsGLB.nhdsWithin_neBot
modified theorem IsLUB.isGLB_of_tendsto
modified theorem isGLB_of_mem_nhds