Structures · Analysis

ESeminormedAddCommMonoid

An e-seminormed commutative monoid is an additive commutative monoid endowed with a continuous enorm. We don't have ESeminormedAddCommMonoid extend EMetricSpace, since the canonical instance ℝ≥0∞ is not an EMetricSpace. This is because ℝ≥0∞ carries the order topology, which is distinct from the topology coming from edist.

Defined in

Mathlib.Analysis.Normed.Group.Defs

Shape

One type argument · adds add_comm