Theorems · Inductive type · functional analysis

ENormedAddCommMonoid

(E : Type u_8) → [TopologicalSpace E] → Type u_8

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

Cited by

32 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpace