Theorems · Inductive type · functional analysis

ESeminormedAddCommMonoid

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

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

Cited by

21 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpace