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

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