Topological (sub)algebras #
A topological algebra over a topological semiring
R is a topological ring with a compatible
continuous scalar multiplication by elements of
R. We reuse typeclass
This is just a minimal stub for now!
The topological closure of a subalgebra is still a subalgebra, which as an algebra is a topological algebra.
The closure of a subalgebra in a topological algebra as a subalgebra.
This is really a statement about topological algebra isomorphisms, but we don't have those, so we use the clunky approach of talking about an algebra homomorphism, and a separate homeomorphism, along with a witness that as functions they are the same.