Theory of proveit.numbers.number_sets

There are three main sets of numbers: integers, reals, and complexes.

import proveit
%theory # toggles between interactive and static modes

Local content of this theory

common expressions	axioms	theorems	demonstrations

Sub-theories

natural_numbers	positive whole numbers starting from zero
integers	positive and negative whole numbers
rational_numbers	ratios of integers
real_numbers	includes irrational numbers (e.g., the square root of 2 is not rational)
complex_numbers	extends real numbers via the imaginary number (square root of -1)

All axioms contained within this theory

This theory contains no axioms directly.

proveit.numbers.number_sets.natural_numbers

proveit.numbers.number_sets.natural_numbers.zero_in_nats

proveit.numbers.number_sets.natural_numbers.successor_in_nats

proveit.numbers.number_sets.natural_numbers.successor_is_injective

proveit.numbers.number_sets.natural_numbers.zero_not_successor

proveit.numbers.number_sets.natural_numbers.induction

proveit.numbers.number_sets.natural_numbers.boolean_natural_membership

proveit.numbers.number_sets.natural_numbers.natural_pos_def

proveit.numbers.number_sets.integers

proveit.numbers.number_sets.integers.integers_def

proveit.numbers.number_sets.integers.integer_interval_is_subset_of_integers

proveit.numbers.number_sets.integers.integer_interval_element_bounds

proveit.numbers.number_sets.rational_numbers

proveit.numbers.number_sets.rational_numbers.rationals_def

proveit.numbers.number_sets.rational_numbers.rationals_pos_def

proveit.numbers.number_sets.rational_numbers.rationals_neg_def

proveit.numbers.number_sets.rational_numbers.rationals_non_neg_def

proveit.numbers.number_sets.real_numbers

proveit.numbers.number_sets.real_numbers.real_pos_def

proveit.numbers.number_sets.real_numbers.in_IntervalOO_def

proveit.numbers.number_sets.real_numbers.in_IntervalOC_def

proveit.numbers.number_sets.real_numbers.in_IntervalCO_def

proveit.numbers.number_sets.real_numbers.in_IntervalCC_def

proveit.numbers.number_sets.complex_numbers

proveit.numbers.number_sets.complex_numbers.imaginary_number_def

proveit.numbers.number_sets.complex_numbers.complex_numbers_def

proveit.numbers.number_sets.complex_numbers.conjugate_def