Expression of type Lambda

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 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 = 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())

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]

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	Lambda	parameter: 66 body: 1
1	Operation	operator: 39 operand: 3
2	ExprTuple	3
3	Lambda	parameters: 4 body: 5
4	ExprTuple	102, 105
5	Conditional	value: 6 condition: 7
6	Operation	operator: 39 operand: 10
7	Operation	operator: 41 operands: 9
8	ExprTuple	10
9	ExprTuple	11, 12
10	Lambda	parameters: 13 body: 14
11	Operation	operator: 73 operands: 15
12	Operation	operator: 73 operands: 16
13	ExprTuple	17, 77, 18
14	Conditional	value: 19 condition: 20
15	ExprTuple	102, 21
16	ExprTuple	105, 21
17	ExprRange	lambda_map: 22 start_index: 104 end_index: 102
18	ExprRange	lambda_map: 23 start_index: 104 end_index: 105
19	Operation	operator: 39 operand: 26
20	Operation	operator: 41 operands: 25
21	Literal
22	Lambda	parameter: 115 body: 78
23	Lambda	parameter: 115 body: 79
24	ExprTuple	26
25	ExprTuple	27, 28, 29
26	Lambda	parameters: 30 body: 31
27	ExprRange	lambda_map: 32 start_index: 104 end_index: 102
28	Operation	operator: 44 operands: 33
29	ExprRange	lambda_map: 34 start_index: 104 end_index: 105
30	ExprTuple	94, 95, 96, 98
31	Conditional	value: 35 condition: 36
32	Lambda	parameter: 115 body: 37
33	ExprTuple	77, 51
34	Lambda	parameter: 115 body: 38
35	Operation	operator: 39 operand: 46
36	Operation	operator: 41 operands: 42
37	Operation	operator: 44 operands: 43
38	Operation	operator: 44 operands: 45
39	Literal
40	ExprTuple	46
41	Literal
42	ExprTuple	47, 48, 49, 50
43	ExprTuple	78, 51
44	Literal
45	ExprTuple	79, 51
46	Lambda	parameter: 97 body: 53
47	ExprRange	lambda_map: 54 start_index: 104 end_index: 102
48	ExprRange	lambda_map: 55 start_index: 104 end_index: 105
49	ExprRange	lambda_map: 56 start_index: 104 end_index: 102
50	ExprRange	lambda_map: 57 start_index: 104 end_index: 105
51	Operation	operator: 58 operand: 66
52	ExprTuple	97
53	Conditional	value: 60 condition: 61
54	Lambda	parameter: 115 body: 62
55	Lambda	parameter: 115 body: 63
56	Lambda	parameter: 115 body: 64
57	Lambda	parameter: 115 body: 65
58	Literal
59	ExprTuple	66
60	Operation	operator: 67 operands: 68
61	Operation	operator: 73 operands: 69
62	Operation	operator: 73 operands: 70
63	Operation	operator: 73 operands: 71
64	Operation	operator: 73 operands: 72
65	Operation	operator: 73 operands: 74
66	Variable
67	Literal
68	ExprTuple	75, 76
69	ExprTuple	97, 77
70	ExprTuple	106, 78
71	ExprTuple	107, 79
72	ExprTuple	108, 78
73	Literal
74	ExprTuple	109, 79
75	Operation	operator: 81 operands: 80
76	Operation	operator: 81 operands: 82
77	Variable
78	IndexedVar	variable: 83 index: 115
79	IndexedVar	variable: 84 index: 115
80	ExprTuple	85, 86
81	Literal
82	ExprTuple	87, 88
83	Variable
84	Variable
85	Operation	operator: 92 operands: 89
86	Operation	operator: 92 operands: 90
87	Operation	operator: 92 operands: 91
88	Operation	operator: 92 operands: 93
89	ExprTuple	94, 95
90	ExprTuple	96, 98
91	ExprTuple	94, 97, 95
92	Literal
93	ExprTuple	96, 97, 98
94	ExprRange	lambda_map: 99 start_index: 104 end_index: 102
95	ExprRange	lambda_map: 100 start_index: 104 end_index: 105
96	ExprRange	lambda_map: 101 start_index: 104 end_index: 102
97	Variable
98	ExprRange	lambda_map: 103 start_index: 104 end_index: 105
99	Lambda	parameter: 115 body: 106
100	Lambda	parameter: 115 body: 107
101	Lambda	parameter: 115 body: 108
102	Variable
103	Lambda	parameter: 115 body: 109
104	Literal
105	Variable
106	IndexedVar	variable: 110 index: 115
107	IndexedVar	variable: 111 index: 115
108	IndexedVar	variable: 112 index: 115
109	IndexedVar	variable: 113 index: 115
110	Variable
111	Variable
112	Variable
113	Variable
114	ExprTuple	115
115	Variable