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, 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 Equals, Forall, Implies, NotEquals
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, 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(), domain = Natural))

# 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(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}\right]\right]

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

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