feat: topological characterization of safety and liveness properties of infinite sequences

[ctchou]

This PR formalizes some results in the following classic paper:

Alpern, Bowen; Schneider, Fred B. (1985). "Defining liveness". Information Processing Letters. 21 (4): 181–185.

To wit:

• By viewing an infinite sequence as an infinite product, we define a topology on infinite sequences using the product topology.
• We identify safety and liveness properties with closed and dense sets in this topology and justify these identifications.
• We prove that every property is the intersection of a safety property and a liveness property and give explicit formulas for both.