Expression of type Lambda ¶

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, Lambda, 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 = Lambda(r, 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())

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

Expression of type Lambda¶

from the theory of proveit.trigonometry¶

Expression of type Lambda ¶

from the theory of proveit.trigonometry ¶