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