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, 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 = 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(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..

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