Theorems · Inductive type · Lie groups

IsSemitopologicalSemiring

(R : Type u_2) → [TopologicalSpace R] → [NonUnitalNonAssocSemiring R] → Prop

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

Cited by

88 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceNonUnitalNonAssocSemiring