Commit 2026-08-12 01:10 3b5417e2

feat(Topology/Order): convergence of suprema and infima (#40578) The main lemma proved in this PR is that for every function a : ι → α, Tendsto (fun F : Finset ι => F.inf a) atTop (𝓝 (⨅ i, a i)), where α is a complete lattice and a SupConvergenceClass. The corresponding versions for ciSup, iInf, ciInf are also proved. We also prove ciSup_eq_ciSup_finset, which is the analogue of iSup_eq_iSup_finset Created with the help of codex.