Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
non-negative_rational_number [2013/08/12 15:11]
nikolaj
non-negative_rational_number [2014/03/21 11:11] (current)
Line 1: Line 1:
 ===== Non-negative rational number ===== ===== Non-negative rational number =====
-==== Definition ​==== +==== Set ==== 
-$ \mathbb Q_+ $ ^+| @#FFBB00: definiendum | @#​FFBB00: ​r \in\mathbb Q_+ $ |
  
-| $ n,m\in \mathbb ​N $ | +@#55CCEE: context ​    | @#​55CCEE: ​\in \mathbb ​$ |
-| $ m>​1 ​$ |+
  
-^ $ \mathbb N \cup \{r\ |\ \exists n,m\ (\ r=\langle n,m\rangle \land \mathrm{gcd}(n,​m)\neq 1\ )\} $ ^ +@#55EE55postulate ​  @#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) & \mathrm{if}\ \mathrm{red}(b,​a)=1\\\\ \langle\mathrm{red}(a,​b),​\mathrm{red}(b,​a)\rangle & \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]]
- +==== Parents ​==== 
-Mizar: [[http://​mizar.org/​JFM/​pdf/​arytm_3.pdf|ARYTM_3]] +=== Refinement of === 
- +[[Non-negative real number]]
-==== Context ​==== +
-Set+
 === Subset of === === Subset of ===
-[[Non-negative real number]]+[[Rational ​number]]
Link to graph
Log In
Improvements of the human condition