logo

Expression of type Conditional

from the theory of proveit.numbers.exponentiation

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, theta
from proveit.logic import And, InSet, NotEquals, NotInSet
from proveit.numbers import Exp, Integer, Mult, Real, e, frac, i, one, pi, two
In [2]:
# build up the expression from sub-expressions
expr = Conditional(NotEquals(Exp(e, Mult(i, theta)), one), And(InSet(theta, Real), NotInSet(frac(theta, Mult(two, pi)), 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())
\left\{\mathsf{e}^{\mathsf{i} \cdot \theta} \neq 1 \textrm{ if } \theta \in \mathbb{R} ,  \frac{\theta}{2 \cdot \pi} \notin \mathbb{Z}\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: 3
operands: 4
2Operationoperator: 5
operands: 6
3Literal
4ExprTuple7, 8
5Literal
6ExprTuple9, 10
7Operationoperator: 11
operands: 12
8Literal
9Operationoperator: 13
operands: 14
10Operationoperator: 15
operands: 16
11Literal
12ExprTuple17, 18
13Literal
14ExprTuple26, 19
15Literal
16ExprTuple20, 21
17Literal
18Operationoperator: 28
operands: 22
19Literal
20Operationoperator: 23
operands: 24
21Literal
22ExprTuple25, 26
23Literal
24ExprTuple26, 27
25Literal
26Variable
27Operationoperator: 28
operands: 29
28Literal
29ExprTuple30, 31
30Literal
31Literal