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

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

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