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 = [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_{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]

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