Select any concept, construction junction, or annotated relation by pointer, touch, search, or keyboard.

Construction junctions are diamonds. They show where multiple structures must coexist on the same carrier and satisfy compatibility conditions.

Canonical static concept record

Seminormed vector space

Open this concept in the interactive graph Read the Markdown equivalent

Summary

A vector space equipped with a seminorm.

Record metadata

Canonical name: Seminormed vector space
Concept ID: seminormed_vector_space
Content version: 2.3.0
Primary field: Mathematics
Fields: Mathematics
Primary domain: Analysis
Domains: Analysis, Topology, Algebra
Alternate terminology: No alternate terminology is currently authored for this record.

Carrier(s)

vector space $V$ over a field $K$ with a specified real-valued absolute value $|\cdot |$

Data

seminorm $p\colon V\to[0,\infty)$

Axioms / constraints

$p(x+y)\le p(x)+p(y)$
$p(\lambda x)=|\lambda |p(x)$

Canonically induces

Pseudometric $d(x,y)=p(x-y)$
topology

Notes

More general value-group-valued norms require a different codomain and axioms; this node records the real-valued analytic notion.

Concept sources

Wikipedia — Seminorm — Seminorm · encyclopedic reference · source ID wp-seminormed-vector-space
Mathlib — Seminorms — Seminorms · formal reference · source ID mathlib-seminorm
Mathlib — Normed modules — Normed modules · formal reference · source ID mathlib-normed-module

Incoming relations (arrows to this concept)

Each relation below ends at this concept.

Vector space Seminormed vector space

Permalink to relation

This is an authored directed relation from the source endpoint to the target endpoint.

Relation ID: e_vector_seminorm
Relation type: Add data add-data
Direction: source → target
Endpoint roles: source: Builds toward; target: Built from
Authored annotation: + real-valued absolute value and seminorm

Authored explanation

Equip the scalar field with a real-valued absolute value $|\cdot|$ and choose $p\colon V\to[0,\infty)$ with $p(x+y)\le p(x)+p(y)$ and $p(\lambda x)=|\lambda|p(x)$ .

How to interpret this relation type

Equip an existing carrier or structured object with additional chosen data, when such compatible data exists. Use a construction junction when several independently meaningful inputs must coexist on the same carrier or interact compatibly.

Relation sources

Mathlib — Seminorms — Seminorms · formal reference · source ID mathlib-seminorm
Mathlib — Normed modules — Normed modules · formal reference · source ID mathlib-normed-module

Outgoing relations (arrows from this concept)

Each relation below starts at this concept.