Expression of type Conditional

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 Conditional, ExprRange, IndexedVar, K, U, V, Variable, W, 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 And, Equals, Forall, Implies, InClass, NotEquals
from proveit.numbers import one

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = VecSpaces(K)
expr = Conditional(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(), And(ExprRange(sub_expr1, InClass(IndexedVar(U, sub_expr1), sub_expr2), one, i), InClass(V, sub_expr2), ExprRange(sub_expr1, InClass(IndexedVar(W, sub_expr1), sub_expr2), one, k)))

expr:

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

\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} \textrm{ if } \left(U_{1} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  \left(U_{2} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  \ldots ,  \left(U_{i} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  V \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right), \left(W_{1} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  \left(W_{2} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right) ,  \ldots ,  \left(W_{k} \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right)\right..

stored_expr.style_options()

name	description	default	current value	related methods
condition_delimiter	'comma' or 'and'	comma	comma	('with_comma_delimiter', 'with_conjunction_delimiter')

# display the expression information
stored_expr.expr_info()

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