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, InSet, Set
from proveit.numbers import Complex, Interval, NaturalPos, 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(n, Conditional(Forall(instance_param_or_params = [Hspace], instance_expr = 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(), domain = HilbertSpaces, condition = Equals(Dim(Hspace), n)).with_wrapping(), InSet(n, NaturalPos))))

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(n \mapsto \left\{\begin{array}{l}\forall_{\mathcal{H} \underset{{\scriptscriptstyle c}}{\in} \textrm{HilbertSpaces}~|~\textrm{Dim}\left(\mathcal{H}\right) = n}~\\
\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}\right]\end{array} \textrm{ if } n \in \mathbb{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: 136 body: 3
2	ExprTuple	136
3	Conditional	value: 4 condition: 5
4	Operation	operator: 13 operand: 8
5	Operation	operator: 121 operands: 7
6	ExprTuple	8
7	ExprTuple	136, 9
8	Lambda	parameter: 78 body: 10
9	Literal
10	Conditional	value: 11 condition: 12
11	Operation	operator: 13 operand: 16
12	Operation	operator: 82 operands: 15
13	Literal
14	ExprTuple	16
15	ExprTuple	17, 18
16	Lambda	parameters: 49 body: 19
17	Operation	operator: 20 operands: 21
18	Operation	operator: 91 operands: 22
19	Conditional	value: 23 condition: 24
20	Literal
21	ExprTuple	78, 25
22	ExprTuple	26, 136
23	Operation	operator: 27 operands: 28
24	Operation	operator: 82 operands: 29
25	Literal
26	Operation	operator: 30 operand: 78
27	Literal
28	ExprTuple	31, 32
29	ExprTuple	33, 34, 35, 36
30	Literal
31	Operation	operator: 91 operands: 37
32	Operation	operator: 61 operand: 45
33	Operation	operator: 121 operands: 39
34	Operation	operator: 121 operands: 40
35	Operation	operator: 91 operands: 41
36	Operation	operator: 91 operands: 42
37	ExprTuple	43, 44
38	ExprTuple	45
39	ExprTuple	95, 56
40	ExprTuple	97, 56
41	ExprTuple	46, 95
42	ExprTuple	47, 97
43	Operation	operator: 48 operands: 49
44	Operation	operator: 50 operand: 56
45	Lambda	parameters: 70 body: 52
46	Operation	operator: 54 operand: 95
47	Operation	operator: 54 operand: 97
48	Literal
49	ExprTuple	95, 97
50	Literal
51	ExprTuple	56
52	Conditional	value: 57 condition: 58
53	ExprTuple	95
54	Literal
55	ExprTuple	97
56	Operation	operator: 59 operands: 60
57	Operation	operator: 61 operand: 64
58	Operation	operator: 121 operands: 63
59	Literal
60	ExprTuple	78, 78
61	Literal
62	ExprTuple	64
63	ExprTuple	65, 66
64	Lambda	parameters: 67 body: 68
65	Operation	operator: 69 operands: 70
66	Operation	operator: 71 operand: 78
67	ExprTuple	73, 74
68	Conditional	value: 75 condition: 76
69	Literal
70	ExprTuple	77
71	Literal
72	ExprTuple	78
73	ExprRange	lambda_map: 79 start_index: 135 end_index: 136
74	ExprRange	lambda_map: 80 start_index: 135 end_index: 136
75	Operation	operator: 82 operands: 81
76	Operation	operator: 82 operands: 83
77	ExprRange	lambda_map: 84 start_index: 135 end_index: 136
78	Variable
79	Lambda	parameter: 117 body: 108
80	Lambda	parameter: 117 body: 109
81	ExprTuple	85, 86
82	Literal
83	ExprTuple	87, 88
84	Lambda	parameter: 117 body: 89
85	Operation	operator: 91 operands: 90
86	Operation	operator: 91 operands: 92
87	ExprRange	lambda_map: 93 start_index: 135 end_index: 136
88	ExprRange	lambda_map: 94 start_index: 135 end_index: 136
89	IndexedVar	variable: 141 index: 117
90	ExprTuple	95, 96
91	Literal
92	ExprTuple	97, 98
93	Lambda	parameter: 117 body: 99
94	Lambda	parameter: 117 body: 100
95	Variable
96	Operation	operator: 102 operand: 106
97	Variable
98	Operation	operator: 102 operand: 107
99	Operation	operator: 121 operands: 104
100	Operation	operator: 121 operands: 105
101	ExprTuple	106
102	Literal
103	ExprTuple	107
104	ExprTuple	108, 110
105	ExprTuple	109, 110
106	Lambda	parameter: 143 body: 111
107	Lambda	parameter: 143 body: 112
108	IndexedVar	variable: 127 index: 117
109	IndexedVar	variable: 128 index: 117
110	Literal
111	Conditional	value: 114 condition: 116
112	Conditional	value: 115 condition: 116
113	ExprTuple	117
114	Operation	operator: 119 operands: 118
115	Operation	operator: 119 operands: 120
116	Operation	operator: 121 operands: 122
117	Variable
118	ExprTuple	123, 125
119	Literal
120	ExprTuple	124, 125
121	Literal
122	ExprTuple	143, 126
123	IndexedVar	variable: 127 index: 143
124	IndexedVar	variable: 128 index: 143
125	Operation	operator: 129 operands: 130
126	Operation	operator: 131 operands: 132
127	Variable
128	Variable
129	Literal
130	ExprTuple	133, 134
131	Literal
132	ExprTuple	135, 136
133	Operation	operator: 137 operand: 140
134	Operation	operator: 138 operand: 140
135	Literal
136	Variable
137	Literal
138	Literal
139	ExprTuple	140
140	IndexedVar	variable: 141 index: 143
141	Variable
142	ExprTuple	143
143	Variable