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, ExprRange, IndexedVar, K, Lambda, U, V, Variable, W, 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, InClass, NotEquals
from proveit.numbers import one

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = VecSpaces(K)
expr = Lambda([U_1_to_i, V, W_1_to_k], Conditional(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(), And(ExprRange(sub_expr1, InClass(IndexedVar(U, sub_expr1), sub_expr2), one, i), InClass(V, sub_expr2), ExprRange(sub_expr1, InClass(IndexedVar(W, sub_expr1), sub_expr2), one, k))))

# 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(U_{1}, U_{2}, \ldots, U_{i}, V, W_{1}, W_{2}, \ldots, W_{k}\right) \mapsto \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} \textrm{ if } \left(U_{1} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  \left(U_{2} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  \ldots ,  \left(U_{i} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  V \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right), \left(W_{1} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  \left(W_{2} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  \ldots ,  \left(W_{k} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right)\right..

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

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

Expression of type Lambda¶

from the theory of proveit.linear_algebra.tensors¶

Expression of type Lambda ¶

from the theory of proveit.linear_algebra.tensors ¶