Commit 2023-12-08 14:37 c04ed1c4

View on Github →

feat: 3 small filter lemmas (#8898)

Written by @PatrickMassot in #7851
Needed for #7851

Estimated changes

Modified Mathlib/Order/LiminfLimsup.lean

added theorem Filter.liminf_comp

added theorem Filter.limsup_comp

Modified Mathlib/Topology/Basic.lean

added theorem isClosed_iff_forall_filter