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 A, B, Conditional, ExprTuple, Lambda, i, n
from proveit.core_expr_types import a_1_to_n, a_i, b_1_to_n, b_i, v_1_to_n, v_i
from proveit.linear_algebra import Adj, Commutator, Dim, HilbertSpaces, Hspace, LinMap, OrthoNormBases, ScalarMult, VecSum, VecZero
from proveit.logic import And, Equals, Exists, Forall, Iff, InClass, InSet, Set
from proveit.numbers import Complex, Interval, one
from proveit.physics.quantum import Bra, Ket, Qmult

# build up the expression from sub-expressions
sub_expr1 = [i]
sub_expr2 = LinMap(Hspace, Hspace)
sub_expr3 = Interval(one, n)
sub_expr4 = Qmult(Ket(v_i), Bra(v_i))
expr = ExprTuple(Lambda(Hspace, Conditional(Forall(instance_param_or_params = [A, B], instance_expr = Iff(Equals(Commutator(A, B), VecZero(sub_expr2)), Exists(instance_param_or_params = [v_1_to_n], instance_expr = Exists(instance_param_or_params = [a_1_to_n, b_1_to_n], instance_expr = And(Equals(A, VecSum(index_or_indices = sub_expr1, summand = ScalarMult(a_i, sub_expr4), domain = sub_expr3)), Equals(B, VecSum(index_or_indices = sub_expr1, summand = ScalarMult(b_i, sub_expr4), domain = sub_expr3))).with_wrapping_at(2), domain = Complex).with_wrapping(), condition = InSet(Set(v_1_to_n), OrthoNormBases(Hspace))).with_wrapping()).with_wrapping_at(2), domain = sub_expr2, conditions = [Equals(Adj(A), A), Equals(Adj(B), B)]).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_{A, B \in \mathcal{L}\left(\mathcal{H}, \mathcal{H}\right)~|~A^{\dagger} = A, B^{\dagger} = B}~\\
\left(\begin{array}{c} \begin{array}{l} \left(\left[A, B\right] = \vec{0}\left(\mathcal{L}\left(\mathcal{H}, \mathcal{H}\right)\right)\right) \Leftrightarrow  \\ \left[\begin{array}{l}\exists_{v_{1}, v_{2}, \ldots, v_{n}~|~\left\{v_{1}, v_{2}, \ldots, v_{n}\right\} \in \textrm{O.N.Bases}\left(\mathcal{H}\right)}~\\
\left[\begin{array}{l}\exists_{a_{1}, a_{2}, \ldots, a_{n}, b_{1}, b_{2}, \ldots, b_{n} \in \mathbb{C}}~\\
\left(\begin{array}{c} \left(A = \left(\sum_{i=1}^{n} \left(a_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right) \land  \\ \left(B = \left(\sum_{i=1}^{n} \left(b_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right) \end{array}\right)\end{array}\right]\end{array}\right] \end{array} \end{array}\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: 70 body: 2
2	Conditional	value: 3 condition: 4
3	Operation	operator: 5 operand: 8
4	Operation	operator: 74 operands: 7
5	Literal
6	ExprTuple	8
7	ExprTuple	9, 10
8	Lambda	parameters: 41 body: 11
9	Operation	operator: 12 operands: 13
10	Operation	operator: 83 operands: 14
11	Conditional	value: 15 condition: 16
12	Literal
13	ExprTuple	70, 17
14	ExprTuple	18, 128
15	Operation	operator: 19 operands: 20
16	Operation	operator: 74 operands: 21
17	Literal
18	Operation	operator: 22 operand: 70
19	Literal
20	ExprTuple	23, 24
21	ExprTuple	25, 26, 27, 28
22	Literal
23	Operation	operator: 83 operands: 29
24	Operation	operator: 53 operand: 37
25	Operation	operator: 113 operands: 31
26	Operation	operator: 113 operands: 32
27	Operation	operator: 83 operands: 33
28	Operation	operator: 83 operands: 34
29	ExprTuple	35, 36
30	ExprTuple	37
31	ExprTuple	87, 48
32	ExprTuple	89, 48
33	ExprTuple	38, 87
34	ExprTuple	39, 89
35	Operation	operator: 40 operands: 41
36	Operation	operator: 42 operand: 48
37	Lambda	parameters: 62 body: 44
38	Operation	operator: 46 operand: 87
39	Operation	operator: 46 operand: 89
40	Literal
41	ExprTuple	87, 89
42	Literal
43	ExprTuple	48
44	Conditional	value: 49 condition: 50
45	ExprTuple	87
46	Literal
47	ExprTuple	89
48	Operation	operator: 51 operands: 52
49	Operation	operator: 53 operand: 56
50	Operation	operator: 113 operands: 55
51	Literal
52	ExprTuple	70, 70
53	Literal
54	ExprTuple	56
55	ExprTuple	57, 58
56	Lambda	parameters: 59 body: 60
57	Operation	operator: 61 operands: 62
58	Operation	operator: 63 operand: 70
59	ExprTuple	65, 66
60	Conditional	value: 67 condition: 68
61	Literal
62	ExprTuple	69
63	Literal
64	ExprTuple	70
65	ExprRange	lambda_map: 71 start_index: 127 end_index: 128
66	ExprRange	lambda_map: 72 start_index: 127 end_index: 128
67	Operation	operator: 74 operands: 73
68	Operation	operator: 74 operands: 75
69	ExprRange	lambda_map: 76 start_index: 127 end_index: 128
70	Variable
71	Lambda	parameter: 109 body: 100
72	Lambda	parameter: 109 body: 101
73	ExprTuple	77, 78
74	Literal
75	ExprTuple	79, 80
76	Lambda	parameter: 109 body: 81
77	Operation	operator: 83 operands: 82
78	Operation	operator: 83 operands: 84
79	ExprRange	lambda_map: 85 start_index: 127 end_index: 128
80	ExprRange	lambda_map: 86 start_index: 127 end_index: 128
81	IndexedVar	variable: 133 index: 109
82	ExprTuple	87, 88
83	Literal
84	ExprTuple	89, 90
85	Lambda	parameter: 109 body: 91
86	Lambda	parameter: 109 body: 92
87	Variable
88	Operation	operator: 94 operand: 98
89	Variable
90	Operation	operator: 94 operand: 99
91	Operation	operator: 113 operands: 96
92	Operation	operator: 113 operands: 97
93	ExprTuple	98
94	Literal
95	ExprTuple	99
96	ExprTuple	100, 102
97	ExprTuple	101, 102
98	Lambda	parameter: 135 body: 103
99	Lambda	parameter: 135 body: 104
100	IndexedVar	variable: 119 index: 109
101	IndexedVar	variable: 120 index: 109
102	Literal
103	Conditional	value: 106 condition: 108
104	Conditional	value: 107 condition: 108
105	ExprTuple	109
106	Operation	operator: 111 operands: 110
107	Operation	operator: 111 operands: 112
108	Operation	operator: 113 operands: 114
109	Variable
110	ExprTuple	115, 117
111	Literal
112	ExprTuple	116, 117
113	Literal
114	ExprTuple	135, 118
115	IndexedVar	variable: 119 index: 135
116	IndexedVar	variable: 120 index: 135
117	Operation	operator: 121 operands: 122
118	Operation	operator: 123 operands: 124
119	Variable
120	Variable
121	Literal
122	ExprTuple	125, 126
123	Literal
124	ExprTuple	127, 128
125	Operation	operator: 129 operand: 132
126	Operation	operator: 130 operand: 132
127	Literal
128	Variable
129	Literal
130	Literal
131	ExprTuple	132
132	IndexedVar	variable: 133 index: 135
133	Variable
134	ExprTuple	135
135	Variable