Theorem operator_function of type Forall

from the theory of proveit.physics.quantum.algebra

see dependencies

import proveit
# Automation is not needed when only building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_theorem_expr # Load the stored theorem expression as 'stored_expr'
# import the special expression
from proveit.physics.quantum.algebra import operator_function

# check that the built expression is the same as the stored expression
assert operator_function.expr == stored_expr
assert operator_function.expr._style_id == stored_expr._style_id
print("Passed sanity check: operator_function matches stored_expr")

Passed sanity check: operator_function matches stored_expr

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\forall_{n \in \mathbb{N}^+}~\left[\begin{array}{l}\forall_{\mathcal{H} \underset{{\scriptscriptstyle c}}{\in} \textrm{HilbertSpaces}~|~\textrm{Dim}\left(\mathcal{H}\right) = n}~\\
\left[\begin{array}{l}\forall_{v_{1}, v_{2}, \ldots, v_{n}~|~\left\{\left\{\lvert v_{1} \rangle, \lvert v_{2} \rangle, \ldots, \lvert v_{n} \rangle\right\}\right\} \in \textrm{O.N.Bases}\left(\mathcal{H}\right)}~\\
\left[\forall_{a_{1}, a_{2}, \ldots, a_{n} \in \mathbb{C}}~\left[\forall_{f \in \left[\mathbb{C} \rightarrow \mathbb{C}\right]}~\left(f\left(\sum_{i=1}^{n} \left(a_{i} \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right) = \left(\sum_{i=1}^{n} \left(f\left(a_{i}\right) \cdot \left(\lvert v_{i} \rangle \thinspace \langle v_{i} \rvert\right)\right)\right)\right)\right]\right]\end{array}\right]\end{array}\right]

stored_expr.style_options()

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',)

# display the expression information
stored_expr.expr_info()

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