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, 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 And, Equals, Forall, Implies, InSet, NotEquals
from proveit.numbers import Natural

# build up the expression from sub-expressions
expr = Conditional(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(), And(InSet(i, Natural), InSet(k, Natural)))

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