Simplification in Semi-continuous real ?

Question

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$

Answer 1

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