Theorem unitarity_by_ortho_norm_bases_elements 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 unitarity_by_ortho_norm_bases_elements

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

Passed sanity check: unitarity_by_ortho_norm_bases_elements 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[\forall_{U \in \mathbb{C}^{n \times 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(\mathbb{C}^{n}\right)}~\\
\left(\left[\forall_{i, j \in \{1~\ldotp \ldotp~n\}}~\left(\left(\langle v_{i} \rvert \thinspace U^{\dagger} \thinspace U \thinspace \lvert v_{j} \rangle\right) = \delta_{i, j}\right)\right] \Rightarrow \left(U \in \textrm{U}\left(n\right)\right)\right)\end{array}\right]\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: 32 operand: 2
1	ExprTuple	2
2	Lambda	parameter: 89 body: 3
3	Conditional	value: 4 condition: 5
4	Operation	operator: 32 operand: 8
5	Operation	operator: 68 operands: 7
6	ExprTuple	8
7	ExprTuple	89, 9
8	Lambda	parameter: 86 body: 10
9	Literal
10	Conditional	value: 11 condition: 12
11	Operation	operator: 32 operand: 15
12	Operation	operator: 68 operands: 14
13	ExprTuple	15
14	ExprTuple	86, 16
15	Lambda	parameters: 17 body: 18
16	Operation	operator: 19 operands: 20
17	ExprTuple	21
18	Conditional	value: 22 condition: 23
19	Literal
20	NamedExprs	field: 52 rows: 89 columns: 89
21	ExprRange	lambda_map: 24 start_index: 88 end_index: 89
22	Operation	operator: 25 operands: 26
23	Operation	operator: 68 operands: 27
24	Lambda	parameter: 90 body: 75
25	Literal
26	ExprTuple	28, 29
27	ExprTuple	30, 31
28	Operation	operator: 32 operand: 38
29	Operation	operator: 68 operands: 34
30	Operation	operator: 45 operand: 40
31	Operation	operator: 36 operand: 41
32	Literal
33	ExprTuple	38
34	ExprTuple	86, 39
35	ExprTuple	40
36	Literal
37	ExprTuple	41
38	Lambda	parameters: 66 body: 42
39	Operation	operator: 43 operand: 89
40	Operation	operator: 45 operands: 46
41	Operation	operator: 47 operands: 48
42	Conditional	value: 49 condition: 50
43	Literal
44	ExprTuple	89
45	Literal
46	ExprTuple	51
47	Literal
48	ExprTuple	52, 89
49	Operation	operator: 53 operands: 54
50	Operation	operator: 55 operands: 56
51	ExprRange	lambda_map: 57 start_index: 88 end_index: 89
52	Literal
53	Literal
54	ExprTuple	58, 59
55	Literal
56	ExprTuple	60, 61
57	Lambda	parameter: 90 body: 62
58	Operation	operator: 63 operands: 64
59	Operation	operator: 65 operands: 66
60	Operation	operator: 68 operands: 67
61	Operation	operator: 68 operands: 69
62	Operation	operator: 80 operand: 75
63	Literal
64	ExprTuple	71, 72, 86, 73
65	Literal
66	ExprTuple	94, 95
67	ExprTuple	94, 74
68	Literal
69	ExprTuple	95, 74
70	ExprTuple	75
71	Operation	operator: 76 operand: 85
72	Operation	operator: 78 operand: 86
73	Operation	operator: 80 operand: 87
74	Operation	operator: 82 operands: 83
75	IndexedVar	variable: 92 index: 90
76	Literal
77	ExprTuple	85
78	Literal
79	ExprTuple	86
80	Literal
81	ExprTuple	87
82	Literal
83	ExprTuple	88, 89
84	ExprTuple	90
85	IndexedVar	variable: 92 index: 94
86	Variable
87	IndexedVar	variable: 92 index: 95
88	Literal
89	Variable
90	Variable
91	ExprTuple	94
92	Variable
93	ExprTuple	95
94	Variable
95	Variable