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, e
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

# build up the expression from sub-expressions
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()

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

\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}

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