By the **extreme value theorem** I take it that you mean that

Every continuous real-valued function on a closed bounded interval is bounded and attains its bounds.

I am going to answer this in terms of *General Topology unsullied by excluded middle* first and consider the meanings of the topological terms and the foundational options afterwards.

Any closed bounded interval is compact and any continuous image of a compact subspace is compact.

I am not aware of any setting that questions these two assertions, so the main question says, in part:

Every compact subspace $K\subset\mathbb R$ is bounded and has a maximum.

For this, clearly $K$ must be non-empty. I claim that it is reasonable to define a compact subspace to be *non-empty* (or, as I call it **occupied**) if $(K\subset\emptyset)=\bot$.

Then $K$ is covered by the (directed) union $\bigcup_n(-n,n)$, so one of these suffices and provides a bound.

Whether there is a *maximum* depends on our definitions of the words *compact* and *maximum*
and in particular of what a *real number* is, to serve as the maximum.

Also, the main question also asks whether the maximimum value is *attained*.

To see why it need not be, consider the function $f:[0,2\pi]\to\mathbb R$ given by $f(x) = a \sin x$, which attains its maximum value at $\pi/2$ if $a>0$ or at $3\pi/2$ if $a<0$. However, if $a$ is so close to $0$ that we do not know its sign (because it depends on some unsolved problem) then we don't know where $f$ attains its bound. Imagine $f$ as a standing wave or as a skipping rope. (Seasoned intuitionists will see that there is actually no logical problem here, but will be able to manufacture a more complicated genuine counterexample.)

Now we turn to the definitional and foundational issues that are needed to make sense of this.

Please be aware that there is no *party line* in constructive mathematics: for perfectly good intellectual reasons, different people study different systems.

Desite being the person who drew Mikhail Katz's attention to **Sythetic Differential Geometry** (aka **Smooth Infinitessimal Analysis**) I am going to leave it to the experts in that to answer the specific question, although I suspect that this will be the same as in locale theory or ASD.

The **Bishop school** does not use the *finite open sub-cover* definition of compactness; for them, a compact subspace is one that is **closed and totally bounded**. Thus is because of issues with the **Fan Theorem**, although that does not bear heavily on this particular question. More relevant is that, for Bishop, the word *compact* carries more properties than I would want.

My answer is based on my system, **Abstract Stone Duality**, and specifically on my paper *A Lambda Calculus for Real Analysis*, which addresses the Intermediate and Extreme Value Theorems. I believe that the situation for **Locale Theory** and **Formal Topology** is the same.

We use the *finite open sub-cover* definition of compactness. This means that the predicate $K\subset U$ is a Scott-continuous function of the open subspace $U$ valued in the Sierpinski space. In locale theory, for the inclusion map $i:K\hookrightarrow\mathbb R$, the direrect image map $i_*$ preserves directed joins.

In this setting, the equations $(K\subset\emptyset)=\bot$ and $i_*\bot=\bot$ are reasonable definitions of a non-empty or **occupied compact subspace**, since they are lattice duals of the definition $\exists_i\top=\top$ for an **inhabited overt subspace**.

However, we need to be careful with the definition of a real number in order to say that such a subspace has a maximum.

By a **real number** $x\in\mathbb R$ we mean a **Dedekind cut**, which is a pair of continuous Sierpinski-valued predicates $(\delta d,\upsilon u)$ saying whether a number $d$ is a lower bound and $u$ is an upper bound. When a "real number" is said to be **uncomputable** or **not constructively defined**, usually what is meant is that one of these predicates is not available. Indeed, we have

Every occupied compact subspace of $\mathbb R$ has a maximum element, as an *upper* real number.

The problem is that the *finite open sub-cover* definition of compactness, on its own, gives no information about lower bounds of the upper bound. However, Bishop has

Every closed, inhabited, totally bounded subspace of $\mathbb R$ has a maximum element, as a Dedekind cut,

whilst I would say that

Every inhabited compact overt subspace of $\mathbb R$ has a maximum element, as a Dedekind cut.

I am not going to give the definition of **overt subspace** here but instead direct you to my MO answer saying why classical mathematicians should care about this idea.

In the case of a compact overt subspace, it is decidable whether it is empty or not and the notions of being inhabited and occupied coincide.

Most familiar (sub)spaces are overt, so to understand the idea (and the constructive status of the Intermediate and Extreme Value Theorems) you need examples of *non-overt* subspaces, which you will find in my paper cited above.

In the good case, how do we find *where* the function attains its bounds? We want to consider the inverse image of the maximum and would like this to be another non-empty compact overt subspace.

In a compact Hausdorff space, closed and compact subspaces are the same. The same is true of open and overt subspaces of an overt *discrete* space, but $\mathbb R$ is not discrete. This means that we have to ask when the inverse image of an overt subspace is overt. This question is the main focus of my paper and my MO answer cited above.

questionif you wish to pursue it. $\endgroup$ – Mikhail Katz Aug 20 '14 at 8:02