Database
BASIC TOPOLOGY
Metric subcomplex vector spaces
Subcomplex pre-Hilbert spaces
ctcph
Next ⟩
df-cph
Metamath Proof Explorer
Unicode
Structured
Syntax definition
ctcph
Description:
Function to put a norm on a pre-Hilbert space.
Ref
Expression
Assertion
ctcph
class toCPreHil