Expression of type Forall ¶

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, 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 = Forall(instance_param_or_params = [K], instance_expr = 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))

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

\forall_{K}~\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()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	None/False	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

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

Expression of type Forall¶

from the theory of proveit.linear_algebra.tensors¶

Expression of type Forall ¶

from the theory of proveit.linear_algebra.tensors ¶