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