Expression of type Conditional ¶

from the theory of proveit.trigonometry ¶

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, a, b, r
from proveit.logic import Equals, Forall, InSet
from proveit.numbers import Abs, Exp, Mult, Real, RealNonNeg, e, frac, i, subtract, two
from proveit.trigonometry import Sin

# build up the expression from sub-expressions
expr = Conditional(Forall(instance_param_or_params = [a, b], instance_expr = Equals(Abs(subtract(Mult(r, Exp(e, Mult(i, a))), Mult(r, Exp(e, Mult(i, b))))), Mult(two, r, Sin(frac(Abs(subtract(a, b)), two)))), domain = Real), InSet(r, RealNonNeg))

# 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\{\forall_{a, b \in \mathbb{R}}~\left(\left|\left(r \cdot \mathsf{e}^{\mathsf{i} \cdot a}\right) - \left(r \cdot \mathsf{e}^{\mathsf{i} \cdot b}\right)\right| = \left(2 \cdot r \cdot \sin{\frac{\left|a - b\right|}{2}}\right)\right) \textrm{ if } r \in \mathbb{R}^{\ge 0}\right..

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions
0	Conditional	value: 1 condition: 2
1	Operation	operator: 3 operand: 6
2	Operation	operator: 23 operands: 5
3	Literal
4	ExprTuple	6
5	ExprTuple	47, 7
6	Lambda	parameters: 8 body: 9
7	Literal
8	ExprTuple	57, 64
9	Conditional	value: 10 condition: 11
10	Operation	operator: 12 operands: 13
11	Operation	operator: 14 operands: 15
12	Literal
13	ExprTuple	16, 17
14	Literal
15	ExprTuple	18, 19
16	Operation	operator: 44 operand: 25
17	Operation	operator: 59 operands: 21
18	Operation	operator: 23 operands: 22
19	Operation	operator: 23 operands: 24
20	ExprTuple	25
21	ExprTuple	41, 47, 26
22	ExprTuple	57, 27
23	Literal
24	ExprTuple	64, 27
25	Operation	operator: 53 operands: 28
26	Operation	operator: 29 operand: 33
27	Literal
28	ExprTuple	31, 32
29	Literal
30	ExprTuple	33
31	Operation	operator: 59 operands: 34
32	Operation	operator: 61 operand: 39
33	Operation	operator: 36 operands: 37
34	ExprTuple	47, 38
35	ExprTuple	39
36	Literal
37	ExprTuple	40, 41
38	Operation	operator: 51 operands: 42
39	Operation	operator: 59 operands: 43
40	Operation	operator: 44 operand: 49
41	Literal
42	ExprTuple	55, 46
43	ExprTuple	47, 48
44	Literal
45	ExprTuple	49
46	Operation	operator: 59 operands: 50
47	Variable
48	Operation	operator: 51 operands: 52
49	Operation	operator: 53 operands: 54
50	ExprTuple	63, 57
51	Literal
52	ExprTuple	55, 56
53	Literal
54	ExprTuple	57, 58
55	Literal
56	Operation	operator: 59 operands: 60
57	Variable
58	Operation	operator: 61 operand: 64
59	Literal
60	ExprTuple	63, 64
61	Literal
62	ExprTuple	64
63	Literal
64	Variable

Expression of type Conditional¶

from the theory of proveit.trigonometry¶

Expression of type Conditional ¶

from the theory of proveit.trigonometry ¶