Sign up ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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 ).

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$
share|cite|improve this question
Have a look at Davorin Lešnik's PhD thesis, available at He has an extensive treatment of reals, done constructively and without countable choice. I think he speaks about lower reals as well. –  Andrej Bauer Sep 25 '12 at 13:00
Please write down the definition of a one-sided cut because it is easy to get that wrong in an intuitionistic setting. –  Andrej Bauer Sep 25 '12 at 13:01
Thank you for this reference. I edited my question to include the definition of a cut. –  Simon Henry Sep 25 '12 at 14:52
I fixed your definition to make it prettier (but probably equivalent to what you had). –  Andrej Bauer Sep 25 '12 at 17:23
I confirm : this is equivalent. –  Simon Henry Sep 25 '12 at 22:31

1 Answer 1

up vote 1 down vote accepted

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

share|cite|improve this answer
I do not understand the definition of $1_U$. What does it mean to take the union of $q < 1$ and $U \cap q < 1$? What does it mean to take the intersection of $U$ and $q < 1$? Are you thinking of $U$ as a truth value, and then $\cup$ and $\cap$ are disjunction and conjunction? Ah, that must be it. So your $1_U$ is $0$ if $U$ is false and $1$ if $U$ is true (but of course that is not a definition). –  Andrej Bauer Sep 27 '12 at 12:33
exactly, I'm thinking of U, q<0 and q<1 as truth value. and $1_U$ is the indicator function. Maybe I should edit to replace $\cup$ by $\vee$ and $\cap$ bu $\wedge$. –  Simon Henry Sep 27 '12 at 12:41
I would rewrite your proof a bit. Might do. –  Andrej Bauer Sep 27 '12 at 17:16

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.