Expression of type ExprTuple

from the theory of proveit.linear_algebra.tensors

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, ExprRange, ExprTuple, IndexedVar, K, Lambda, U, V, Variable, W, b, e, i, k
from proveit.core_expr_types import U_1_to_i, W_1_to_k, a_1_to_i, c_1_to_k, d_1_to_i, f_1_to_k
from proveit.linear_algebra import TensorProd, VecSpaces, VecZero
from proveit.logic import And, Equals, Forall, Implies, InClass, NotEquals
from proveit.numbers import one

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = VecSpaces(K)
expr = ExprTuple(Lambda([U_1_to_i, V, W_1_to_k], Conditional(Forall(instance_param_or_params = [a_1_to_i, c_1_to_k, d_1_to_i, f_1_to_k], instance_expr = Forall(instance_param_or_params = [b, e], instance_expr = Implies(Equals(TensorProd(a_1_to_i, b, c_1_to_k), TensorProd(d_1_to_i, e, f_1_to_k)).with_wrapping_at(2), Equals(TensorProd(a_1_to_i, c_1_to_k), TensorProd(d_1_to_i, f_1_to_k)).with_wrapping_at(2)).with_wrapping_at(2), domain = V, conditions = [Equals(b, e), NotEquals(b, VecZero(V))]), domains = [U_1_to_i, W_1_to_k, U_1_to_i, W_1_to_k]).with_wrapping(), And(ExprRange(sub_expr1, InClass(IndexedVar(U, sub_expr1), sub_expr2), one, i), InClass(V, sub_expr2), ExprRange(sub_expr1, InClass(IndexedVar(W, sub_expr1), sub_expr2), one, k)))))

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(\left(U_{1}, U_{2}, \ldots, U_{i}, V, W_{1}, W_{2}, \ldots, W_{k}\right) \mapsto \left\{\begin{array}{l}\forall_{\left(a_{1} \in U_{1}\right), \left(a_{2} \in U_{2}\right), \ldots, \left(a_{i} \in U_{i}\right),\left(c_{1} \in W_{1}\right), \left(c_{2} \in W_{2}\right), \ldots, \left(c_{k} \in W_{k}\right),\left(d_{1} \in U_{1}\right), \left(d_{2} \in U_{2}\right), \ldots, \left(d_{i} \in U_{i}\right),\left(f_{1} \in W_{1}\right), \left(f_{2} \in W_{2}\right), \ldots, \left(f_{k} \in W_{k}\right)}~\\
\left[\forall_{b, e \in V~|~b = e, b \neq \vec{0}\left(V\right)}~\left(\begin{array}{c} \begin{array}{l} \left(\begin{array}{c} \begin{array}{l} \left(a_{1} {\otimes}  a_{2} {\otimes}  \ldots {\otimes}  a_{i} {\otimes} b{\otimes} c_{1} {\otimes}  c_{2} {\otimes}  \ldots {\otimes}  c_{k}\right) =  \\ \left(d_{1} {\otimes}  d_{2} {\otimes}  \ldots {\otimes}  d_{i} {\otimes} e{\otimes} f_{1} {\otimes}  f_{2} {\otimes}  \ldots {\otimes}  f_{k}\right) \end{array} \end{array}\right) \Rightarrow  \\ \left(\begin{array}{c} \begin{array}{l} \left(a_{1} {\otimes}  a_{2} {\otimes}  \ldots {\otimes}  a_{i}{\otimes} c_{1} {\otimes}  c_{2} {\otimes}  \ldots {\otimes}  c_{k}\right) =  \\ \left(d_{1} {\otimes}  d_{2} {\otimes}  \ldots {\otimes}  d_{i}{\otimes} f_{1} {\otimes}  f_{2} {\otimes}  \ldots {\otimes}  f_{k}\right) \end{array} \end{array}\right) \end{array} \end{array}\right)\right]\end{array} \textrm{ if } \left(U_{1} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  \left(U_{2} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  \ldots ,  \left(U_{i} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  V \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right), \left(W_{1} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  \left(W_{2} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  \ldots ,  \left(W_{k} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right)\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	parameters: 2 body: 3
2	ExprTuple	4, 96, 5
3	Conditional	value: 6 condition: 7
4	ExprRange	lambda_map: 8 start_index: 102 end_index: 100
5	ExprRange	lambda_map: 9 start_index: 102 end_index: 103
6	Operation	operator: 25 operand: 12
7	Operation	operator: 53 operands: 11
8	Lambda	parameter: 113 body: 65
9	Lambda	parameter: 113 body: 66
10	ExprTuple	12
11	ExprTuple	13, 14, 15
12	Lambda	parameters: 16 body: 17
13	ExprRange	lambda_map: 18 start_index: 102 end_index: 100
14	Operation	operator: 29 operands: 19
15	ExprRange	lambda_map: 20 start_index: 102 end_index: 103
16	ExprTuple	92, 93, 94, 95
17	Conditional	value: 21 condition: 22
18	Lambda	parameter: 113 body: 23
19	ExprTuple	96, 36
20	Lambda	parameter: 113 body: 24
21	Operation	operator: 25 operand: 31
22	Operation	operator: 53 operands: 27
23	Operation	operator: 29 operands: 28
24	Operation	operator: 29 operands: 30
25	Literal
26	ExprTuple	31
27	ExprTuple	32, 33, 34, 35
28	ExprTuple	65, 36
29	Literal
30	ExprTuple	66, 36
31	Lambda	parameters: 73 body: 37
32	ExprRange	lambda_map: 38 start_index: 102 end_index: 100
33	ExprRange	lambda_map: 39 start_index: 102 end_index: 103
34	ExprRange	lambda_map: 40 start_index: 102 end_index: 100
35	ExprRange	lambda_map: 41 start_index: 102 end_index: 103
36	Operation	operator: 42 operand: 50
37	Conditional	value: 44 condition: 45
38	Lambda	parameter: 113 body: 46
39	Lambda	parameter: 113 body: 47
40	Lambda	parameter: 113 body: 48
41	Lambda	parameter: 113 body: 49
42	Literal
43	ExprTuple	50
44	Operation	operator: 51 operands: 52
45	Operation	operator: 53 operands: 54
46	Operation	operator: 70 operands: 55
47	Operation	operator: 70 operands: 56
48	Operation	operator: 70 operands: 57
49	Operation	operator: 70 operands: 58
50	Variable
51	Literal
52	ExprTuple	59, 60
53	Literal
54	ExprTuple	61, 62, 63, 64
55	ExprTuple	104, 65
56	ExprTuple	105, 66
57	ExprTuple	106, 65
58	ExprTuple	107, 66
59	Operation	operator: 72 operands: 67
60	Operation	operator: 72 operands: 68
61	Operation	operator: 70 operands: 69
62	Operation	operator: 70 operands: 71
63	Operation	operator: 72 operands: 73
64	Operation	operator: 74 operands: 75
65	IndexedVar	variable: 76 index: 113
66	IndexedVar	variable: 77 index: 113
67	ExprTuple	78, 79
68	ExprTuple	80, 81
69	ExprTuple	90, 96
70	Literal
71	ExprTuple	91, 96
72	Literal
73	ExprTuple	90, 91
74	Literal
75	ExprTuple	90, 82
76	Variable
77	Variable
78	Operation	operator: 86 operands: 83
79	Operation	operator: 86 operands: 84
80	Operation	operator: 86 operands: 85
81	Operation	operator: 86 operands: 87
82	Operation	operator: 88 operand: 96
83	ExprTuple	92, 90, 93
84	ExprTuple	94, 91, 95
85	ExprTuple	92, 93
86	Literal
87	ExprTuple	94, 95
88	Literal
89	ExprTuple	96
90	Variable
91	Variable
92	ExprRange	lambda_map: 97 start_index: 102 end_index: 100
93	ExprRange	lambda_map: 98 start_index: 102 end_index: 103
94	ExprRange	lambda_map: 99 start_index: 102 end_index: 100
95	ExprRange	lambda_map: 101 start_index: 102 end_index: 103
96	Variable
97	Lambda	parameter: 113 body: 104
98	Lambda	parameter: 113 body: 105
99	Lambda	parameter: 113 body: 106
100	Variable
101	Lambda	parameter: 113 body: 107
102	Literal
103	Variable
104	IndexedVar	variable: 108 index: 113
105	IndexedVar	variable: 109 index: 113
106	IndexedVar	variable: 110 index: 113
107	IndexedVar	variable: 111 index: 113
108	Variable
109	Variable
110	Variable
111	Variable
112	ExprTuple	113
113	Variable