Commit 2024-07-13 19:14 eed869b6

View on Github →

feat(Order.LiminfLimsup): add limsup_max (#14564) Add characterization of limsup and limsup of max.

Estimated changes

modified theorem csInf_univ
added theorem Filter.le_liminf_iff
added theorem Filter.le_limsup_iff
added theorem Filter.liminf_le_iff
added theorem Filter.limsup_le_iff
added theorem liminf_finset_inf'
added theorem liminf_finset_inf
added theorem liminf_min
added theorem limsup_finset_sup'
added theorem limsup_finset_sup
added theorem limsup_max