logo

Expression of type Conditional

from the theory of proveit.numbers.modular

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 Conditional, L, S, c, x
from proveit.logic import Card, Equals, Forall, InSet, SetOfAll, SubsetEq
from proveit.numbers import Add, Mod, Real
In [2]:
# build up the expression from sub-expressions
sub_expr1 = [x]
expr = Conditional(Forall(instance_param_or_params = [S], instance_expr = Forall(instance_param_or_params = [c], instance_expr = Equals(Card(SetOfAll(instance_param_or_params = sub_expr1, instance_element = Mod(Add(c, x), L), domain = S)), Card(SetOfAll(instance_param_or_params = sub_expr1, instance_element = Mod(x, L), domain = S))), domain = Real), condition = SubsetEq(S, Real)), InSet(L, Real))
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())
\left\{\forall_{S~|~S \subseteq \mathbb{R}}~\left[\forall_{c \in \mathbb{R}}~\left(|\left\{\left(c + x\right) ~\textup{mod}~ L\right\}_{x \in S}| = |\left\{x ~\textup{mod}~ L\right\}_{x \in S}|\right)\right] \textrm{ if } L \in \mathbb{R}\right..
In [5]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
condition_delimiter'comma' or 'and'commacomma('with_comma_delimiter', 'with_conjunction_delimiter')
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Conditionalvalue: 1
condition: 2
1Operationoperator: 10
operand: 5
2Operationoperator: 44
operands: 4
3ExprTuple5
4ExprTuple47, 24
5Lambdaparameter: 48
body: 7
6ExprTuple48
7Conditionalvalue: 8
condition: 9
8Operationoperator: 10
operand: 14
9Operationoperator: 12
operands: 13
10Literal
11ExprTuple14
12Literal
13ExprTuple48, 24
14Lambdaparameter: 51
body: 16
15ExprTuple51
16Conditionalvalue: 17
condition: 18
17Operationoperator: 19
operands: 20
18Operationoperator: 44
operands: 21
19Literal
20ExprTuple22, 23
21ExprTuple51, 24
22Operationoperator: 26
operand: 28
23Operationoperator: 26
operand: 29
24Literal
25ExprTuple28
26Literal
27ExprTuple29
28Operationoperator: 31
operand: 33
29Operationoperator: 31
operand: 34
30ExprTuple33
31Literal
32ExprTuple34
33Lambdaparameter: 52
body: 35
34Lambdaparameter: 52
body: 37
35Conditionalvalue: 38
condition: 40
36ExprTuple52
37Conditionalvalue: 39
condition: 40
38Operationoperator: 42
operands: 41
39Operationoperator: 42
operands: 43
40Operationoperator: 44
operands: 45
41ExprTuple46, 47
42Literal
43ExprTuple52, 47
44Literal
45ExprTuple52, 48
46Operationoperator: 49
operands: 50
47Variable
48Variable
49Literal
50ExprTuple51, 52
51Variable
52Variable