Structures · Analysis

NormedSpace

A normed space over a normed field is a vector space endowed with a norm which satisfies the equality ‖c • x‖ = ‖c‖ ‖x‖. We require only ‖c • x‖ ≤ ‖c‖ ‖x‖ in the definition, then prove ‖c • x‖ = ‖c‖ ‖x‖ in norm_smul. Note that since this requires SeminormedAddCommGroup and not NormedAddCommGroup, this typeclass can be used for "seminormed spaces" too, just as Module can be used for "semimodules".

Defined in

Mathlib.Analysis.Normed.Module.Basic

Shape

2 explicit arguments · adds norm_smul_le