Structures · Analysis

ENormedAddCommMonoid

An enormed commutative monoid is an additive commutative monoid endowed with a continuous enorm which is positive definite. We don't have ENormedAddCommMonoid 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 enorm_eq_zero