Hi !


I'm considering in a general topos $T$ the object $R$ of lower semi-continuous real (one sided lower non-empty Dedekind cuts, as for exemple in <http://ncatlab.org/nlab/show/one-sided+real+number> ).


I want to know if, even if substraction is not possible, there is (internally) some sort of simplification rules for addition like :


If $x$ is 'bounded' (there exist a rational q such that $x \leqslant q$ ) then $x+a=x+b$ imply $a=b$.


It's seem true to me, but only because of an argument involving a covering of $T$ by a boolean topos, if it's possible I would prefer a completely internal argument, and I can't find it.


[Edited by Andrej Bauer] A lower Dedekind cut is a subset $L \subseteq \mathbb{Q}$ which is


* **rounded:** $q \in L \iff \exists r \in L . q < r$
* **inhabited** $\exists q \in \mathbb{Q} . q \in L$
* **bounded:** $\exists q \in \mathbb{Q} \forall r \in L . r < q$



Simplification in Semi-continuous real ?
Ok I think I finally found an internaly valid proof by my self, so I explain it briefly here in case someone is interested some day :


If $U \in \Omega$ is a subterminal object, you can define the element $1\_U \in R$ as :


$q \in 1\_U$ when $q < 0 \cup (U \cap q<1)$.


(this correspond to the indicator function of an open set... )


It's easy to show that if $x+1\_U \leqslant y + 1\_U$ then $x \leqslant y$ :


if $q < x$, then $q < x+1\_U$, hence, $\exists u,v$ such that $q=u+v, u < y$ and $v < 0 \cup (v<1 \cap U)$


* First case : $v<0$ then, $q < u < y$, we have $q < y$.
* Second case : we have 'U' then $1\_U = 1$ so $q+1 < x+1\_U$, 


$q+1 < y +1$


$q < y$


In both case, $q < y$ so $x \leqslant y$.


Now, if $x$ is any bounded positive element, let $N$ be an integer such that $x < N$.


on can define :


$\displaystyle h = \frac{1}{n} \sum\_{i=1}^{N.n } 1\_{x> (i/n)} $


and one can show that (but it's a little longer) :
$h \leqslant x \leqslant h+\frac{1}{n}$.


It's now easy to conclude if $x$ is positive and bounded and $a + x \leqslant x + b$
then if $q < a$, take $q'$ another rational such that $q < q' < a$, let $n$ an integer such that $q'-q < \frac{1}{n}$. and let $h$ be as above :


$ a + h \leqslant a +x \leqslant b+x \leqslant b + h + 1/n $ 


but by a simple recurence, h can be simplified so :


$ a \leqslant b+1/n $


so $q' < b+1/n$, and finaly $q < q'-1/n < b $


If $x$ is not positive, just take some $q < x$, and $x-q$ will be positive


