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 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 Equals, Forall, Implies, NotEquals
from proveit.numbers import Natural

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