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