Right Continuous Functions and Lower Limit Topology

Stream: mathlib4

[Yongxi Lin (Aaron)]

I would like to introduce the notion of lower limit topology. Namely the topology generated by intervals of the form [a,b). The main motivation is that this topology gives a topological characterization of right continuous functions so that we can use theorems about continuous functions for right continuous functions. For example, in the Brownian motion project I want to prove Doob's maximal inequalities for right continuous martingales, and one of the essential lemma is that right continuous functions reaches its supremum on a dense set, which is Dense.ciSup. Potentially this new API about lower limit topology can simplify some proofs in Counterexample.SorgenfreyLine.

However, I should mention that I am still relatively new to Lean and not very familiar with writing an entirely new API. I would appreciate any suggestions on how to approach this and produce a good PR.

[Yongxi Lin (Aaron)]

Here's a draft: https://github.com/leanprover-community/mathlib4/pull/33586. Any suggestions are welcome.

[Yan Yablonovskiy 🇺🇦]

(deleted)