Expression of type ExprTuple

from the theory of proveit.physics.quantum.algebra

import proveit
# Automation is not needed when building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_expr # Load the stored expression as 'stored_expr'
# import Expression classes needed to build the expression
from proveit import Conditional, ExprTuple, Function, Lambda, f, i, n
from proveit.core_expr_types import a_1_to_n, a_i, v_1_to_n, v_i
from proveit.linear_algebra import Dim, HilbertSpaces, Hspace, OrthoNormBases, ScalarMult, VecSum
from proveit.logic import And, Equals, Forall, Functions, InClass, InSet, Set
from proveit.numbers import Complex, Interval, one
from proveit.physics.quantum import Bra, Ket, Qmult
from proveit.physics.quantum.algebra import v_1_to_n_kets

# build up the expression from sub-expressions
sub_expr1 = [i]
sub_expr2 = Interval(one, n)
sub_expr3 = Qmult(Ket(v_i), Bra(v_i))
expr = ExprTuple(Lambda(Hspace, Conditional(Forall(instance_param_or_params = [v_1_to_n], instance_expr = Forall(instance_param_or_params = [a_1_to_n], instance_expr = Forall(instance_param_or_params = [f], instance_expr = Equals(Function(f, [VecSum(index_or_indices = sub_expr1, summand = ScalarMult(a_i, sub_expr3), domain = sub_expr2)]), VecSum(index_or_indices = sub_expr1, summand = ScalarMult(Function(f, [a_i]), sub_expr3), domain = sub_expr2)), domain = Functions(Complex, Complex)), domain = Complex), condition = InSet(Set(v_1_to_n_kets), OrthoNormBases(Hspace))).with_wrapping(), And(InClass(Hspace, HilbertSpaces), Equals(Dim(Hspace), n)))))

expr:

# check that the built expression is the same as the stored expression
assert expr == stored_expr
assert expr._style_id == stored_expr._style_id
print("Passed sanity check: expr matches stored_expr")

Passed sanity check: expr matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\left(\mathcal{H} \mapsto \left\{\begin{array}{l}\forall_{v_{1}, v_{2}, \ldots, v_{n}~|~\left\{\left\{\lvert v_{1} \rangle, \lvert v_{2} \rangle, \ldots, \lvert v_{n} \rangle\right\}\right\} \in \textrm{O.N.Bases}\left(\mathcal{H}\right)}~\\
\left[\forall_{a_{1}, a_{2}, \ldots, a_{n} \in \mathbb{C}}~\left[\forall_{f \in \left[\mathbb{C} \rightarrow \mathbb{C}\right]}~\left(f\left(\sum_{i=1}^{n} \left(a_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right) = \left(\sum_{i=1}^{n} \left(f\left(a_{i}\right) \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right)\right]\right]\end{array} \textrm{ if } \mathcal{H} \underset{{\scriptscriptstyle c}}{\in} \textrm{HilbertSpaces} ,  \textrm{Dim}\left(\mathcal{H}\right) = n\right..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	ExprTuple	1
1	Lambda	parameter: 36 body: 2
2	Conditional	value: 3 condition: 4
3	Operation	operator: 38 operand: 7
4	Operation	operator: 40 operands: 6
5	ExprTuple	7
6	ExprTuple	8, 9
7	Lambda	parameters: 10 body: 11
8	Operation	operator: 12 operands: 13
9	Operation	operator: 55 operands: 14
10	ExprTuple	15
11	Conditional	value: 16 condition: 17
12	Literal
13	ExprTuple	36, 18
14	ExprTuple	19, 101
15	ExprRange	lambda_map: 20 start_index: 100 end_index: 101
16	Operation	operator: 38 operand: 24
17	Operation	operator: 86 operands: 22
18	Literal
19	Operation	operator: 23 operand: 36
20	Lambda	parameter: 73 body: 64
21	ExprTuple	24
22	ExprTuple	25, 26
23	Literal
24	Lambda	parameters: 27 body: 28
25	Operation	operator: 42 operand: 35
26	Operation	operator: 30 operand: 36
27	ExprTuple	32
28	Conditional	value: 33 condition: 34
29	ExprTuple	35
30	Literal
31	ExprTuple	36
32	ExprRange	lambda_map: 37 start_index: 100 end_index: 101
33	Operation	operator: 38 operand: 44
34	Operation	operator: 40 operands: 41
35	Operation	operator: 42 operands: 43
36	Variable
37	Lambda	parameter: 73 body: 63
38	Literal
39	ExprTuple	44
40	Literal
41	ExprTuple	45
42	Literal
43	ExprTuple	46
44	Lambda	parameter: 88 body: 48
45	ExprRange	lambda_map: 49 start_index: 100 end_index: 101
46	ExprRange	lambda_map: 50 start_index: 100 end_index: 101
47	ExprTuple	88
48	Conditional	value: 51 condition: 52
49	Lambda	parameter: 73 body: 53
50	Lambda	parameter: 73 body: 54
51	Operation	operator: 55 operands: 56
52	Operation	operator: 86 operands: 57
53	Operation	operator: 86 operands: 58
54	Operation	operator: 102 operand: 64
55	Literal
56	ExprTuple	60, 61
57	ExprTuple	88, 62
58	ExprTuple	63, 72
59	ExprTuple	64
60	Operation	operator: 88 operand: 70
61	Operation	operator: 74 operand: 71
62	Operation	operator: 67 operands: 68
63	IndexedVar	variable: 97 index: 73
64	IndexedVar	variable: 106 index: 73
65	ExprTuple	70
66	ExprTuple	71
67	Literal
68	ExprTuple	72, 72
69	ExprTuple	73
70	Operation	operator: 74 operand: 77
71	Lambda	parameter: 108 body: 76
72	Literal
73	Variable
74	Literal
75	ExprTuple	77
76	Conditional	value: 78 condition: 82
77	Lambda	parameter: 108 body: 79
78	Operation	operator: 84 operands: 80
79	Conditional	value: 81 condition: 82
80	ExprTuple	83, 90
81	Operation	operator: 84 operands: 85
82	Operation	operator: 86 operands: 87
83	Operation	operator: 88 operand: 92
84	Literal
85	ExprTuple	92, 90
86	Literal
87	ExprTuple	108, 91
88	Variable
89	ExprTuple	92
90	Operation	operator: 93 operands: 94
91	Operation	operator: 95 operands: 96
92	IndexedVar	variable: 97 index: 108
93	Literal
94	ExprTuple	98, 99
95	Literal
96	ExprTuple	100, 101
97	Variable
98	Operation	operator: 102 operand: 105
99	Operation	operator: 103 operand: 105
100	Literal
101	Variable
102	Literal
103	Literal
104	ExprTuple	105
105	IndexedVar	variable: 106 index: 108
106	Variable
107	ExprTuple	108
108	Variable