Demonstrations for the theory of proveit.numbers.number_sets.rational_numbers ¶

import proveit
from proveit import q, p, r, s, x

from proveit import defaults
from proveit.logic.equality import equals_reversal

from proveit.logic import Boolean, NotEquals, InSet, ProperSubset
from proveit.numbers import Less, LessEq, greater, greater_eq, zero
from proveit.numbers import (
    Natural, NaturalPos, Integer, IntegerNonZero, IntegerNeg, IntegerNonPos,
    Rational, RationalNonZero, RationalPos, RationalNeg, RationalNonNeg, RationalNonPos)
from proveit.numbers.number_sets.rational_numbers  import rationals_def
%begin demonstrations

The Rational Numbers, $\mathbb{Q}$ and Various Subsets $\mathbb{Q}^{+}$, $\mathbb{Q}^{-}$, $\mathbb{Q}^{\ge 0}$ [Under Construction]¶

Introduction
Simple Expressions involving the Rational Numbers $\mathbb{Q}$
Common Attributes of the Rational Numbers NumberSet $\mathbb{Q}$
Axioms
Theorems & Conjectures
Further Demonstrations

TBA
TBA
TBA

Miscellaneous Testing

Introduction ¶

TBA

Simple Expressions involving the Rational Numbers $\mathbb{Q}$¶

It is straightforward to construct expressions involving the Rational Numbers NumberSet $\mathbb{Q}$:

# a simple set membership claim
InSet(x, Rational)

ProperSubset(Natural, RationalNonNeg)

Common Attributes of the Rational Numbers NumberSet $\mathbb{Q}$¶

TBA Placeholder — attributes not particularly relevant for NumberSet …

# the Rational number set
Rational

Axioms ¶

The ``axioms`` for the Rational Numbers $\mathbb{Q}$ … can be accessed on the [rational axioms](./_axioms_.ipynb) page, and establish the definitions of the Rational numbers and various subsets of the Rational numbers.

# def of the Rational number set
rationals_def

Theorems & Conjectures ¶

The `number/sets/rational` theory already has a substantial number of related theorems and conjectures established, covering a wide range of … The remainder can be found in the [containment theorems notebook](./\_theorems\_.ipynb).

from proveit.numbers.number_sets.rational_numbers import (zero_is_rational)

zero_is_rational

Demonstrations ¶

1. TBA

We begin with …

2. TBA.

TBA

3. TBA

TBA

Miscellaneous Testing¶

The material below was developed to test various Rational NumberSet-related methods. Some of this material could be integrated into the `_demonstrations_` page eventually and/or deleted as development continues.

Testing the `InSet` class methods related to the Rational Numbers and its subsets¶

<font size =3>The InSet class has a deduce_in_bool() method that eventually depends on the deduce_membership_in_bool() method of the underlying NumberSet class.
</font>

q_in_Q = InSet(q, Rational)

q_in_Q.deduce_in_bool()

p_in_QPos = InSet(p, RationalPos)

p_in_QPos.deduce_in_bool()

r_in_QNeg = InSet(p, RationalNeg)

r_in_QNeg.deduce_in_bool()

s_in_QNonNeg = InSet(s, RationalNonNeg)

s_in_QNonNeg.deduce_in_bool()

Number set membership demonstrations¶

InSet(InSet(r, Rational), Boolean).prove()

InSet(InSet(r, RationalNonZero), Boolean).prove()

InSet(InSet(r, RationalPos), Boolean).prove()

InSet(InSet(r, RationalNeg), Boolean).prove()

InSet(InSet(r, RationalNonNeg), Boolean).prove()

InSet(InSet(r, RationalNonPos), Boolean).prove()

NotEquals(r, zero).prove(assumptions=[InSet(r, RationalNonZero)], 
                         conclude_automation=False) # should be side-effect

greater(x, zero).prove(assumptions=[InSet(x, RationalPos)], 
                       conclude_automation=False) # should be side-effect

Less(x, zero).prove(assumptions=[InSet(x, RationalNeg)], 
                    conclude_automation=False) # should be side-effect

greater_eq(x, zero).prove(assumptions=[InSet(x, RationalNonNeg)], 
                          conclude_automation=False) # should be side-effect

LessEq(x, zero).prove(assumptions=[InSet(x, RationalNonPos)], 
                      conclude_automation=False) # should be side-effect

InSet(r, RationalNonZero).prove(assumptions=[InSet(r, Rational), NotEquals(r, zero)])

InSet(r, RationalPos).prove(assumptions=[InSet(r, Rational), greater(r, zero)])

InSet(r, RationalNeg).prove(assumptions=[InSet(r, Rational), Less(r, zero)])

InSet(r, RationalNonNeg).prove(assumptions=[InSet(r, Rational), greater_eq(r, zero)])

InSet(r, RationalNonPos).prove(assumptions=[InSet(r, Rational), LessEq(r, zero)])

InSet(r, RationalNonNeg).prove(assumptions=[InSet(r, Natural)])

InSet(r, RationalPos).prove(assumptions=[InSet(r, NaturalPos)])

InSet(r, Rational).prove(assumptions=[InSet(r, Integer)])

InSet(r, RationalNonZero).prove(assumptions=[InSet(r, IntegerNonZero)])

InSet(r, RationalNeg).prove(assumptions=[InSet(r, IntegerNeg)])

InSet(r, RationalNonPos).prove(assumptions=[InSet(r, IntegerNonPos)])

InSet(r, Rational).prove(assumptions=[InSet(r, RationalNonZero)])

InSet(r, Rational).prove(assumptions=[InSet(r, RationalPos)])

InSet(r, RationalNonZero).prove(assumptions=[InSet(r, RationalPos)])

InSet(r, RationalNeg).prove(assumptions=[InSet(r, IntegerNeg)])

InSet(r, RationalNonNeg).prove(assumptions=[InSet(r, RationalPos)])

InSet(r, Rational).prove(assumptions=[InSet(r, RationalNeg)])

InSet(r, RationalNonZero).prove(assumptions=[InSet(r, RationalNeg)])

InSet(r, RationalNonPos).prove(assumptions=[InSet(r, RationalNeg)])

InSet(r, Rational).prove(assumptions=[InSet(r, RationalNonNeg)])

InSet(r, Rational).prove(assumptions=[InSet(r, RationalNonPos)])

%end demonstrations

Demonstrations for the theory of proveit.numbers.number_sets.rational_numbers¶