Theorem is_open_lt_fst_snd

feat(topology): restructure order topologies; (start) proof that ennreal is a topological monoid

Merge branch 'master' of https://github.com/leanprover/mathlib

refactor(data/finset): fix formatting issues

feat(topology): add topological structures for groups, ring, and linear orders; add instances for rat and real