Commit 2026-03-21 15:22 10214d2e

View on Github →

feat(Order/Filter/AtTopBot/Tendsto): use to_dual (#36823) This PR uses to_dual on some theorems about atTop and atBot

Estimated changes

deleted theorem Filter.OrderBot.atBot_eq
deleted theorem Filter.tendsto_atBot
deleted theorem Filter.tendsto_atBot_mono
deleted theorem Filter.tendsto_atBot_pure