Expression of type Lambda ¶

from the theory of proveit.numbers.summation ¶

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 Function, Lambda, a, b, c, f, fx, x
from proveit.logic import Equals, Forall
from proveit.numbers import Add, Integer, Interval, Sum, subtract

# build up the expression from sub-expressions
sub_expr1 = [x]
expr = Lambda(f, Forall(instance_param_or_params = [a, b, c], instance_expr = Equals(Sum(index_or_indices = sub_expr1, summand = fx, domain = Interval(a, b)), Sum(index_or_indices = sub_expr1, summand = Function(f, [subtract(x, c)]), domain = Interval(Add(a, c), Add(b, c)))), domain = Integer))

# 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())

f \mapsto \left[\forall_{a, b, c \in \mathbb{Z}}~\left(\left(\sum_{x = a}^{b} f\left(x\right)\right) = \left(\sum_{x = a + c}^{b + c} f\left(x - c\right)\right)\right)\right]

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

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

Expression of type Lambda¶

from the theory of proveit.numbers.summation¶

Expression of type Lambda ¶

from the theory of proveit.numbers.summation ¶