User:Dfeuer/To Do

From ProofWiki
Jump to navigation Jump to search

Refactor and rework the definitions for the usual topology on the real line and real vector spaces.

The current arrangement defines the Euclidean metrics for real vector spaces and (as a special case, essentially) the complex numbers, which is a valuable thing to do. It also separately defines a Euclidean metric for powers of $\Q$, which seems silly. But then it goes and defines a "Euclidean topology" for $\R^n$ based on the Euclidean metrics, and this makes much less sense.

1. There's nothing particularly Euclidean about it: hyperbolic geometry, for example, induces the same topology.

2. Some texts (e.g., Kelley and Munkres) introduce the usual topology on the reals in order-theoretic terms (it is the order topology, and because the reals are unbounded above and below that gives the order topology a basis of open intervals). Then the usual topology on $\R^S$ is defined as the product topology, and the Euclidean metric is shown to induce it in the finite-dimensional case. --Dfeuer (talk) 18:48, 25 February 2013 (UTC)

The great importance of these definitions leads me to ask that you proceed on the basis of preferably multiple sources which you undoubtedly possess — otherwise, drop me a note; I can probably provide you with a few. Among these sources, those already mentioned on PW should be considered first, of course. — Lord_Farin (talk) 19:09, 25 February 2013 (UTC)
I don't have terribly many, but I can use them. We actually already have most of the information here on PW—it's just arranged in a very metric-centered way (presumably the influence of Sutherland). Most of what I'm talking about is rearranging it to make the order-based approach a coequal one rather than a secondary one. Some proofs (I don't remember which) will want alternative versions added to take advantage of the other perspective. --Dfeuer (talk) 19:14, 25 February 2013 (UTC)
Ok. In due time I'll monitor and comment; please give me a heads up when you're about to start (and I'd then also appreciate a more detailed outline of what you envisage). — Lord_Farin (talk) 19:18, 25 February 2013 (UTC)