Commit 2025-02-10 19:23 e790abc2

chore(Order/Filter): split AtTopBot.lean (#21672) This PR splits Order/Filter/AtTopBot.lean into the following files:

• Order/Filter/AtTopBot/Defs.lean: definition and elementary properties
• Order/Filter/AtTopBot/Disjoint.lean: showing AtTop and AtBot are disjoint
• Order/Filter/AtTopBot/Tendsto.lean: basic limits of AtTop and AtBot
• Order/Filter/AtTopBot/CompleteLattice.lean: results in a (conditionally) complete lattice
• Order/Filter/AtTopBot/Finset.lean: results involving finite sets
• Order/Filter/AtTopBot/Map.lean: results involving map/comap
• Order/Filter/AtTopBot/Prod.lean: results involving product of filters
• Order/Filter/AtTopBot/Basic.lean: remaining results (those depending on Order.Filter.Bases) The goal is to reduce the dependencies for Topology.Basic. The results are not too exciting for the file itself, but we do get some nice cleanups down the line.