Metamath Proof Explorer

Definition df-ehl

Description: Define a function generating the real Euclidean spaces of finite dimension. The case n = 0 corresponds to a space of dimension 0, that is, limited to a neutral element (see ehl0 ). Members of this family of spaces are Hilbert spaces, as shown in - ehlhl . (Contributed by Thierry Arnoux, 16-Jun-2019)

Ref Expression
Assertion df-ehl 
|- EEhil = ( n e. NN0 |-> ( RR^ ` ( 0 ..^ n ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cehl 
 |-  EEhil
1 vn 
 |-  n
2 cn0 
 |-  NN0
3 crrx 
 |-  RR^
4 cc0 
 |-  0
5 cfzo 
 |-  ..^
6 1 cv 
 |-  n
7 4 6 5 co 
 |-  ( 0 ..^ n )
8 7 3 cfv 
 |-  ( RR^ ` ( 0 ..^ n ) )
9 1 2 8 cmpt 
 |-  ( n e. NN0 |-> ( RR^ ` ( 0 ..^ n ) ) )
10 0 9 wceq 
 |-  EEhil = ( n e. NN0 |-> ( RR^ ` ( 0 ..^ n ) ) )