logo

Expression of type Forall

from the theory of proveit.numbers.summation

In [1]:
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, a, b, c, f, fx, x
from proveit.logic import Equals, Forall
from proveit.numbers import Add, Integer, Interval, Sum, subtract
In [2]:
# build up the expression from sub-expressions
sub_expr1 = [x]
expr = Forall(instance_param_or_params = [f], instance_expr = 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))
expr:
In [3]:
# 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
In [4]:
# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())
\forall_{f}~\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]
In [5]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
with_wrappingIf 'True', wrap the Expression after the parametersNoneNone/False('with_wrapping',)
condition_wrappingWrap 'before' or 'after' the condition (or None).NoneNone/False('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_paramsIf 'True', wraps every two parameters AND wraps the Expression after the parametersNoneNone/False('with_params',)
justificationjustify to the 'left', 'center', or 'right' in the array cellscentercenter('with_justification',)
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Operationoperator: 5
operand: 2
1ExprTuple2
2Lambdaparameter: 38
body: 4
3ExprTuple38
4Operationoperator: 5
operand: 7
5Literal
6ExprTuple7
7Lambdaparameters: 8
body: 9
8ExprTuple58, 59, 60
9Conditionalvalue: 10
condition: 11
10Operationoperator: 12
operands: 13
11Operationoperator: 14
operands: 15
12Literal
13ExprTuple16, 17
14Literal
15ExprTuple18, 19, 20
16Operationoperator: 22
operand: 27
17Operationoperator: 22
operand: 28
18Operationoperator: 40
operands: 24
19Operationoperator: 40
operands: 25
20Operationoperator: 40
operands: 26
21ExprTuple27
22Literal
23ExprTuple28
24ExprTuple58, 29
25ExprTuple59, 29
26ExprTuple60, 29
27Lambdaparameter: 49
body: 30
28Lambdaparameter: 49
body: 31
29Literal
30Conditionalvalue: 32
condition: 33
31Conditionalvalue: 34
condition: 35
32Operationoperator: 38
operand: 49
33Operationoperator: 40
operands: 37
34Operationoperator: 38
operand: 43
35Operationoperator: 40
operands: 41
36ExprTuple49
37ExprTuple49, 42
38Variable
39ExprTuple43
40Literal
41ExprTuple49, 44
42Operationoperator: 47
operands: 45
43Operationoperator: 56
operands: 46
44Operationoperator: 47
operands: 48
45ExprTuple58, 59
46ExprTuple49, 50
47Literal
48ExprTuple51, 52
49Variable
50Operationoperator: 53
operand: 60
51Operationoperator: 56
operands: 55
52Operationoperator: 56
operands: 57
53Literal
54ExprTuple60
55ExprTuple58, 60
56Literal
57ExprTuple59, 60
58Variable
59Variable
60Variable