Expression of type ExprTuple

from the theory of proveit.linear_algebra.linear_maps

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, ExprTuple, Function, K, Lambda, P, Px, Py, V, W, c, x, y
from proveit.linear_algebra import LinMap, ScalarMult, VecAdd, VecSpaces
from proveit.logic import And, Equals, Forall, Iff, InClass, InSet

# build up the expression from sub-expressions
sub_expr1 = [x]
sub_expr2 = VecSpaces(K)
expr = ExprTuple(Lambda([V, W], Conditional(Forall(instance_param_or_params = [P], instance_expr = Iff(InSet(P, LinMap(V, W)), And(Forall(instance_param_or_params = sub_expr1, instance_expr = InSet(Px, W), domain = V), Forall(instance_param_or_params = [x, y], instance_expr = Equals(Function(P, [VecAdd(x, y)]), VecAdd(Px, Py)), domain = V), Forall(instance_param_or_params = [c], instance_expr = Forall(instance_param_or_params = sub_expr1, instance_expr = Equals(Function(P, [ScalarMult(c, x)]), ScalarMult(c, Px)), domain = V), domain = K)).with_wrapping_at(2,4)).with_wrapping_at(2)), And(InClass(V, sub_expr2), InClass(W, sub_expr2)))))

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(\left(V, W\right) \mapsto \left\{\forall_{P}~\left(\begin{array}{c} \begin{array}{l} \left(P \in \mathcal{L}\left(V, W\right)\right) \Leftrightarrow  \\ \left(\begin{array}{c} \left[\forall_{x \in V}~\left(P\left(x\right) \in W\right)\right] \land  \\ \left[\forall_{x, y \in V}~\left(P\left(x + y\right) = \left(P\left(x\right) + P\left(y\right)\right)\right)\right] \land  \\ \left[\forall_{c \in K}~\left[\forall_{x \in V}~\left(P\left(c \cdot x\right) = \left(c \cdot P\left(x\right)\right)\right)\right]\right] \end{array}\right) \end{array} \end{array}\right) \textrm{ if } V \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right) ,  W \underset{{\scriptscriptstyle c}}{\in} \textrm{VecSpaces}\left(K\right)\right..\right)

stored_expr.style_options()

no style options

# display the expression information
stored_expr.expr_info()

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