I have added pointer (here) from your paragraph to the reference, so that it does not look like an unbased claim

]]>adding a sentence about the Heine-Borel theorem in dependent type theory using the inductive covers higher inductive type

Anonymous

]]>I have spelled out a classical proof of the *Heine-Borel theorem*, here

Okay, I see. I wasn’t aware of that. I thought I was using a common term.

]]>Yes, “cartesian coordinates” sometimes, but just as often “rectangular coordinates” or just “coordinates”. And not “cartesian space”.

]]>Before reading Mike #8, I reacted to Zoran #7 by editing things in a similar line.

@Urs: Although I very much *like* the term “Cartesian space”, I learnt it only from you. Maybe it’s a German thing?

But you say “cartesian coordinates” in schood, don’t you?

]]>I didn’t learn “coordinate space” or “Cartesian space” in high school or undergraduate. We called it “$\mathbb{R}^n$”.

]]>But wait, “Cartesian space” is a dead standard term no? Here this is taught in high school. Analytic geometry.

Whether you take the maps betwen them to be continuous, smooth or linear depends, no matter how you call it.

]]>Then I would say “a real $n$-dimensional *vector* space”. Maybe one should emphasize “the” ?

“real n-dimensional space” is not unique to $\mathbb{R}^n$ but points to any vector space isomorphic to $\mathbb{R}^n$.

]]>Hmm, I am unfamiliar with “coordinate space” terminology either. Are you then unfamiliar in a similar vain with “real $n$-dimensional space” ?

Urs: I know that it was appearing in a context of smooth spaces, but after not seeing it for a while, I am never sure which one is which (what is the restriction on morphisms, do we count smooth structure or not, and is it for presheaves or for original test spaces). So at first I thought that it is a synonym for a smooth space, thus that the intended theorem is a generalization.

]]>a text with lots of unfamiliar words like Cartesian space

I was not aware that you count “Cartesian space” as an “unfamilar word”!

]]>Guess the most popular name is just “coordinate space” for the $\mathbb{R}^n$’s, because that’s the term you lerned in ’undergraduate’ . Obviously the reason are the base isomorphisms from any vector space into an apropriate $\mathbb{R}^n$.

]]>That is much better. Even more familiar textbook phrase is also “subspace $S$ of real $n$-dimensional space $\mathbf{R}^n$.

]]>What about “Let S be a topological subspace of a Cartesian space, i.e. $S\subseteq \mathbb{R}^n$ for some $n\in\mathbb{N}$”? The “i.e.” clues the reader that nothing more is being said by the first phrase than the second, hence “Cartesian space” must refer to $\mathbb{R}^n$.

]]>Look, it scares me when I see a text with lots of unfamiliar words like Cartesian space. What about people who are much less new-definition and theory friendly, as most mathematicians are ? If a word is not necessary it can be linked in brackets, then one knows it is not important to know it. It looked to me that one is pointing to a more general context of some beasts called Cartesian spaces, to which the classical Heine-Borel is generalized. If Cartesian were in brackets rather than a part of the linear statement, I would neglect it and maybe even learn without clicking. Clicking may be easy for some, but to me, who does more than half of the work from bad connections, sometimes a new loading of a page may mean a couple of minutes freeze of a browser. And yes, I think we should be able to link eventually somehow from symbols (Urs, you were always more of a technology optimist than I, don’t give up this time), even from formulas.

]]>Yes, I agree with Toby. On the $n$Lab I happily link even to terms that I find dead-standard. Because somebody may come who does not know the term.

Maybe better would be in this case here to have the symbol “$\mathbb{R}^N$” be hyperlinked. But that’s not really possible, is it. And not really nicer, either, I find.

You know, it even gives me a little pain each time that an entry says “$let n \in \mathbb{Z}$” without linking to *integer*. Because, optimally, every single technical point would be linked to its explanation. Who knows, next time the 10-year old genius-to-be comes reading our $n$Lab pages and wants to know what $\mathbb{R}^N$ denotes, or what $\mathbb{Z}$ denotes. In any case, links are what a wiki is for. Books without hyperlinks we had enough. And it slowed mankind down for long enough.

You’re not missing anything. I think that the main for saying the words “Cartesian space” is to have something to put the link on. (I forget if Urs or I put those words in.)

The only really standard term for a Cartesian space is the symbol “$\mathbb{R}^n$”, but it’s nice to have a word too, and the concept is closely associated with Descartes. Some people say “Euclidean space”, but that has another meaning which is more appropriate for Euclid (who used no coordinates).

]]>Let $S$ be a topological subspace $S\subset \mathbf{R}^n$ of a Cartesian space.

I find “of a Cartesian space” both superfluous and confusing as it is already written that it is a subset of $\mathbf{R}^n$ and the topology there is standard for most of the Earth’s mathematicians. On the other hand, I have never seen in the literature outside of ncat community expression “Cartesian space” for $\mathbf{R}^n$ and when I read this then I start clicking to find out what it is, as it looks to me that maybe a greater generality is hidden somewhere in the statement. So I was confused when reading the statement.

]]>Thanks, nice!

I have created a stub for *pointless topology* just so as to keep the link from being grey.

I expanded on this in a couple of ways.

]]>stub for *Heine-Borel theorem*