logo

Expression of type Forall

from the theory of proveit.linear_algebra.tensors

In [1]:
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, i, j, k
from proveit.core_expr_types import U_1_to_i, V_1_to_j, W_1_to_k, a_1_to_i, b_1_to_j, c_1_to_k
from proveit.linear_algebra import TensorProd, VecSpaces
from proveit.logic import Equals, Forall
from proveit.numbers import Natural
In [2]:
# build up the expression from sub-expressions
sub_expr1 = [U_1_to_i, V_1_to_j, W_1_to_k]
expr = Forall(instance_param_or_params = [i, j, k], instance_expr = Forall(instance_param_or_params = sub_expr1, instance_expr = Forall(instance_param_or_params = [a_1_to_i, b_1_to_j, c_1_to_k], instance_expr = Equals(TensorProd(a_1_to_i, TensorProd(b_1_to_j), c_1_to_k), TensorProd(a_1_to_i, b_1_to_j, c_1_to_k)).with_wrapping_at(1), domains = sub_expr1).with_wrapping(), domain = VecSpaces(K)).with_wrapping(), domain = Natural)
expr:
In [3]:
# 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
In [4]:
# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())
\forall_{i, j, k \in \mathbb{N}}~\left[\begin{array}{l}\forall_{U_{1}, U_{2}, \ldots, U_{i}, V_{1}, V_{2}, \ldots, V_{j}, 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(b_{1} \in V_{1}\right), \left(b_{2} \in V_{2}\right), \ldots, \left(b_{j} \in V_{j}\right),\left(c_{1} \in W_{1}\right), \left(c_{2} \in W_{2}\right), \ldots, \left(c_{k} \in W_{k}\right)}~\\
\left(\begin{array}{c} \begin{array}{l} \left(a_{1} {\otimes}  a_{2} {\otimes}  \ldots {\otimes}  a_{i} {\otimes} \left(b_{1} {\otimes}  b_{2} {\otimes}  \ldots {\otimes}  b_{j}\right){\otimes} c_{1} {\otimes}  c_{2} {\otimes}  \ldots {\otimes}  c_{k}\right) \\  = \left(a_{1} {\otimes}  a_{2} {\otimes}  \ldots {\otimes}  a_{i}{\otimes} b_{1} {\otimes}  b_{2} {\otimes}  \ldots {\otimes}  b_{j}{\otimes} c_{1} {\otimes}  c_{2} {\otimes}  \ldots {\otimes}  c_{k}\right) \end{array} \end{array}\right)\end{array}\right]\end{array}\right]
In [5]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
with_wrappingIf 'True', wrap the Expression after the parametersNoneNone/False('with_wrapping',)
condition_wrappingWrap 'before' or 'after' the condition (or None).NoneNone/False('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_paramsIf 'True', wraps every two parameters AND wraps the Expression after the parametersNoneNone/False('with_params',)
justificationjustify to the 'left', 'center', or 'right' in the array cellscentercenter('with_justification',)
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Operationoperator: 27
operand: 2
1ExprTuple2
2Lambdaparameters: 3
body: 4
3ExprTuple74, 89, 76
4Conditionalvalue: 5
condition: 6
5Operationoperator: 27
operand: 9
6Operationoperator: 45
operands: 8
7ExprTuple9
8ExprTuple10, 11, 12
9Lambdaparameters: 13
body: 14
10Operationoperator: 79
operands: 15
11Operationoperator: 79
operands: 16
12Operationoperator: 79
operands: 17
13ExprTuple18, 19, 20
14Conditionalvalue: 21
condition: 22
15ExprTuple74, 23
16ExprTuple89, 23
17ExprTuple76, 23
18ExprRangelambda_map: 24
start_index: 88
end_index: 74
19ExprRangelambda_map: 25
start_index: 88
end_index: 89
20ExprRangelambda_map: 26
start_index: 88
end_index: 76
21Operationoperator: 27
operand: 30
22Operationoperator: 45
operands: 29
23Literal
24Lambdaparameter: 98
body: 83
25Lambdaparameter: 98
body: 84
26Lambdaparameter: 98
body: 86
27Literal
28ExprTuple30
29ExprTuple31, 32, 33
30Lambdaparameters: 58
body: 34
31ExprRangelambda_map: 35
start_index: 88
end_index: 74
32ExprRangelambda_map: 36
start_index: 88
end_index: 89
33ExprRangelambda_map: 37
start_index: 88
end_index: 76
34Conditionalvalue: 38
condition: 39
35Lambdaparameter: 98
body: 40
36Lambdaparameter: 98
body: 41
37Lambdaparameter: 98
body: 42
38Operationoperator: 43
operands: 44
39Operationoperator: 45
operands: 46
40Operationoperator: 49
operands: 47
41Operationoperator: 49
operands: 48
42Operationoperator: 49
operands: 50
43Literal
44ExprTuple51, 52
45Literal
46ExprTuple53, 54, 55
47ExprTuple83, 56
48ExprTuple84, 56
49Literal
50ExprTuple86, 56
51Operationoperator: 71
operands: 57
52Operationoperator: 71
operands: 58
53ExprRangelambda_map: 59
start_index: 88
end_index: 74
54ExprRangelambda_map: 60
start_index: 88
end_index: 89
55ExprRangelambda_map: 61
start_index: 88
end_index: 76
56Operationoperator: 62
operand: 70
57ExprTuple65, 64, 66
58ExprTuple65, 81, 66
59Lambdaparameter: 98
body: 67
60Lambdaparameter: 98
body: 68
61Lambdaparameter: 98
body: 69
62Literal
63ExprTuple70
64Operationoperator: 71
operands: 72
65ExprRangelambda_map: 73
start_index: 88
end_index: 74
66ExprRangelambda_map: 75
start_index: 88
end_index: 76
67Operationoperator: 79
operands: 77
68Operationoperator: 79
operands: 78
69Operationoperator: 79
operands: 80
70Variable
71Literal
72ExprTuple81
73Lambdaparameter: 98
body: 82
74Variable
75Lambdaparameter: 98
body: 85
76Variable
77ExprTuple82, 83
78ExprTuple95, 84
79Literal
80ExprTuple85, 86
81ExprRangelambda_map: 87
start_index: 88
end_index: 89
82IndexedVarvariable: 90
index: 98
83IndexedVarvariable: 91
index: 98
84IndexedVarvariable: 92
index: 98
85IndexedVarvariable: 93
index: 98
86IndexedVarvariable: 94
index: 98
87Lambdaparameter: 98
body: 95
88Literal
89Variable
90Variable
91Variable
92Variable
93Variable
94Variable
95IndexedVarvariable: 96
index: 98
96Variable
97ExprTuple98
98Variable