Structures · Topology

IsSemitopologicalSemiring

A semitopological semiring is a semiring R where addition is jointly continuous and multiplication is continuous in each variable separately. We allow for non-unital and non-associative semirings as well. The IsSemitopologicalSemiring class should only be instantiated in the presence of a NonUnitalNonAssocSemiring instance; if there is an instance of NonUnitalNonAssocRing, then IsSemitopologicalRing should be used. Note: in the presence of NonAssocRing, these classes are mathematically equivalent (see IsTopologicalSemiring.continuousNeg_of_mul or IsSemitopologicalSemiring.toIsTopologicalRing).

Defined in

Mathlib.Topology.Algebra.Ring.Basic

Shape

One type argument