Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
non-negative_rational_number [2013/05/19 23:27] nikolaj |
non-negative_rational_number [2013/09/03 00:55] nikolaj |
||
---|---|---|---|
Line 1: | Line 1: | ||
===== Non-negative rational number ===== | ===== Non-negative rational number ===== | ||
==== Definition ==== | ==== Definition ==== | ||
- | ^ $ \mathbb Q_+ $ ^ | + | | @#FFBB00: $ r \in\mathbb Q_+ $ | |
- | | $ n,m\in \mathbb N $ | | + | | @#88DDEE: $ r \in \mathbb Q $ | |
- | | $ m>1 $ | | + | |
- | ^ $ \mathbb N \cup \{r\ |\ \exists n,m\ (\ r=\langle n,m\rangle \land \mathrm{gcd}(n,m)\neq 1\ )\} $ ^ | + | | @#55EE55: $ r \ge 0 $ | |
- | + | ||
- | ==== Ramifications ==== | + | |
- | + | ||
- | === Definitions === | + | |
- | + | ||
- | | $ a,b,c,x\in \mathbb N $ | | + | |
- | | $b\neq 0$ | | + | |
- | | $ r,s,t \in \mathbb Q_+ $ | | + | |
- | + | ||
- | ^ $ a\div b:=x,\hspace{1cm}(c<b)\land (a=x\cdot b+c)$ | | + | |
- | ^ $ \mathrm{red}(a,b):=a\div\mathrm{gcd}(a,b)$ | | + | |
- | + | ||
- | ^ $ \frac{a}{b} \equiv $ | | + | |
- | + | ||
- | \begin{cases} | + | |
- | + | ||
- | \mathrm{red}(a,b)\hspace{1cm}\mathrm{if}\ \mathrm{red}(b,a)=1 | + | |
- | + | ||
- | \langle\mathrm{red}(a,b),\mathrm{red}(b,a)\rangle\hspace{1cm}\mathrm{else} | + | |
- | + | ||
- | \end{cases} | + | |
- | + | ||
- | ^ $ \mathrm{num}\frac{a}{b}\equiv a $ ^ | + | |
- | ^ $ \mathrm{den}\frac{a}{b}\equiv b $ ^ | + | |
- | + | ||
- | ^ $ r+s=\frac{\mathrm{num} r\ \cdot\ \mathrm{den} s\ +\ \mathrm{num} s\ \cdot\ \mathrm{den} r}{\mathrm{den} r\ \cdot\ \mathrm{den} s}$ ^ | + | |
- | ^ $ r\cdot s=\frac{\mathrm{num} r\ \cdot\ \mathrm{num} s}{\mathrm{den} r\ \cdot\ \mathrm{den} s}$ ^ | + | |
- | + | ||
- | === Predicates === | + | |
- | ^ $r\leq s\equiv \exists t\ (s=r+t)$ ^ | + | |
- | ^ $r < s\equiv s\leq r$ ^ | + | |
+ | ==== Discussion ==== | ||
=== Reference === | === Reference === | ||
Wikipedia: [[http://en.wikipedia.org/wiki/Rational_number|Rational number]] | Wikipedia: [[http://en.wikipedia.org/wiki/Rational_number|Rational number]] | ||
- | |||
- | Mizar: [[http://mizar.org/JFM/pdf/arytm_3.pdf|ARYTM_3]] | ||
- | |||
==== Context ==== | ==== Context ==== | ||
- | Set | + | === Refinement of === |
+ | [[Non-negative real number]] | ||
=== Subset of === | === Subset of === | ||
- | [[Non-negative real number]] | + | [[Rational number]] |
- | === Parents === | + | |
- | [[Natural number]], [[Ordered pair]] | + |