Theorems · Inductive type · functional analysis

ContinuousENorm

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

A type E equipped with a continuous map ‖·‖ₑ : E → ℝ≥0∞ NB. We do not demand that the topology is somehow defined by the enorm: for ℝ≥0∞ (the motivating example behind this definition), this is not true.

Defined in

Mathlib.Analysis.Normed.Group.Defs

Cited by

290 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

TopologicalSpace