Commit 2024-09-07 14:24 e56ed5b1

View on Github →

feat(AtTopBot): drop unneeded assumptions (#16571) Drop unneeded IsDirected assumptions in several lemmas.

Estimated changes

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.Frequently.forall_exists_of_atBot

added theorem Filter.Frequently.forall_exists_of_atTop

modified theorem Filter.atTop_basis'

modified theorem Filter.atTop_eq_generate_Ici