Theorems · Inductive type · functional analysis

NormedSpace.Core

(𝕜 : Type u_6) → (E : Type u_7) → [inst : NormedField 𝕜] → [inst_1 : AddCommGroup E] → [Module 𝕜 E] → [Norm E] → Prop

A structure encapsulating minimal axioms needed to defined a normed vector space, as found in textbooks. This is meant to be used to easily define NormedAddCommGroup E and NormedSpace E instances from scratch on a type with no preexisting distance or topology.

Defined in

Mathlib.Analysis.Normed.Module.Basic

Cited by

5 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

NormedFieldAddCommGroupModuleNorm