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

# build up the expression from sub-expressions
expr = 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, 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(), 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(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(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} \textrm{ if } i \in \mathbb{N} ,  k \in \mathbb{N}\right..

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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