This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ 𝔼_{hil} = (n \in ℕ_{0} ⟼ (1 \dots n))$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cehl	$class 𝔼_{hil}$
1		vn	$setvar n$
2		cn0	$class ℕ_{0}$
3		crrx	$class ℝ↑$
4		c1	$class 1$
5		cfz	$class \dots$
6	1	cv	$setvar n$
7	4 6 5	co	$class (1 \dots n)$
8	7 3	cfv	$class (1 \dots n)$
9	1 2 8	cmpt	$class (n \in ℕ_{0} ⟼ (1 \dots n))$
10	0 9	wceq	$wff 𝔼_{hil} = (n \in ℕ_{0} ⟼ (1 \dots n))$