Commit 2024-02-21 16:46 65d9c6c4

View on Github →

feat: add tendsto_atBot_atTop_of_antitone (#10794)

Estimated changes

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.tendsto_atBot_atTop_iff_of_antitone

added theorem Filter.tendsto_atBot_atTop_of_antitone

added theorem Filter.tendsto_atTop_atBot_iff_of_antitone

added theorem Filter.tendsto_atTop_atBot_of_antitone