Commit 2026-01-31 16:38 8405e447
View on Github →feat: generalize some lemmas about linear ordered topological spaces (#33863)
Currently, lemmas about Filter.map ((↑) : Set.Iio a → X) Filter.atTop etc
assume that the ambient type is densely ordered.
However, it suffices to require that a is an Order.IsSuccPrelimit.
Make this generalization and move the lemmas to a new file.
Also, use the new lemmas to drop a [DenselyOrdered _] assumption
in one lemma in measure theory.
These more precise statements are also useful when dealing with, e.g.,
linear ordered topologies defined by ordinals.