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, ExprTuple, K, Lambda, V, 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, InSet, NotEquals
from proveit.numbers import Natural

# build up the expression from sub-expressions
expr = ExprTuple(Lambda([i, k], Conditional(Forall(instance_param_or_params = [U_1_to_i, V, W_1_to_k], instance_expr = 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(), domain = VecSpaces(K)).with_wrapping(), And(InSet(i, Natural), InSet(k, Natural)))))

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