A topological semiring is a semiring where addition and multiplication are continuous.
The (topological-space) closure of a subsemiring of a topological semiring is itself a subsemiring.
The product topology on the cartesian product of two topological semirings makes the product into a topological semiring.
- to_has_continuous_add : has_continuous_add α
- to_has_continuous_mul : has_continuous_mul α
- continuous_neg : continuous (λ (a : α), -a)
A topological ring is a ring where the ring operations are continuous.
The product topology on the cartesian product of two topological rings makes the product into a topological ring.
The (topological-space) closure of a subring of a topological semiring is itself a subring.