Commit 2026-01-20 12:31 59080482

chore(Topology/Order): fix name of nhdsLT lemma (#34063) The dual version of this was renamed over a year and a half ago, and it looks like this one was missed. In particular, all lemmas in mathlib about 𝓝[<] are named nhdsLT with this one as the sole exception, and we choose the new name to match the dual nhdsGT_neBot_of_exists_gt. Note that the statement itself appears different, but is definitionally equal to the old one, and again matches the dual.