logo

Axiom breakup_sum of type Forall

from the theory of proveit.numbers.summation

see dependencies

In [1]:
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_axiom_expr # Load the stored axiom expression as 'stored_expr'
# import the special expression
from proveit.numbers.summation import breakup_sum
In [2]:
# check that the built expression is the same as the stored expression
assert breakup_sum.expr == stored_expr
assert breakup_sum.expr._style_id == stored_expr._style_id
print("Passed sanity check: breakup_sum matches stored_expr")
Passed sanity check: breakup_sum matches stored_expr
In [3]:
# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())
\forall_{a, b, c \in \mathbb{Z}~|~a \leq b \leq c}~\left[\forall_{\alpha}~\left(\left(\sum_{k = a}^{c} \alpha_{k}\right) = \left(\left(\sum_{k = a}^{b} \alpha_{k}\right) + \left(\sum_{k = b + 1}^{c} \alpha_{k}\right)\right)\right)\right]
In [4]:
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 [5]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Operationoperator: 7
operand: 2
1ExprTuple2
2Lambdaparameters: 3
body: 4
3ExprTuple62, 67, 64
4Conditionalvalue: 5
condition: 6
5Operationoperator: 7
operand: 10
6Operationoperator: 20
operands: 9
7Literal
8ExprTuple10
9ExprTuple11, 12, 13, 14
10Lambdaparameter: 52
body: 16
11Operationoperator: 54
operands: 17
12Operationoperator: 54
operands: 18
13Operationoperator: 54
operands: 19
14Operationoperator: 20
operands: 21
15ExprTuple52
16Operationoperator: 22
operands: 23
17ExprTuple62, 24
18ExprTuple67, 24
19ExprTuple64, 24
20Literal
21ExprTuple25, 26
22Literal
23ExprTuple27, 28
24Literal
25Operationoperator: 29
operands: 59
26Operationoperator: 29
operands: 30
27Operationoperator: 38
operand: 33
28Operationoperator: 65
operands: 32
29Literal
30ExprTuple67, 64
31ExprTuple33
32ExprTuple34, 35
33Lambdaparameter: 57
body: 36
34Operationoperator: 38
operand: 41
35Operationoperator: 38
operand: 42
36Conditionalvalue: 48
condition: 40
37ExprTuple41
38Literal
39ExprTuple42
40Operationoperator: 54
operands: 43
41Lambdaparameter: 57
body: 44
42Lambdaparameter: 57
body: 45
43ExprTuple57, 46
44Conditionalvalue: 48
condition: 47
45Conditionalvalue: 48
condition: 49
46Operationoperator: 60
operands: 50
47Operationoperator: 54
operands: 51
48IndexedVarvariable: 52
index: 57
49Operationoperator: 54
operands: 55
50ExprTuple62, 64
51ExprTuple57, 56
52Variable
53ExprTuple57
54Literal
55ExprTuple57, 58
56Operationoperator: 60
operands: 59
57Variable
58Operationoperator: 60
operands: 61
59ExprTuple62, 67
60Literal
61ExprTuple63, 64
62Variable
63Operationoperator: 65
operands: 66
64Variable
65Literal
66ExprTuple67, 68
67Variable
68Literal