Talk:Closed Bounded Subset of Real Numbers is Compact/Proof 1

From ProofWiki
Jump to navigation Jump to search

Perhaps a "Closed [and bounded] interval in $\R$ is compact" page could be extracted from this, if it doesn't exist already? --Plammens (talk) 14:36, 14 April 2021 (UTC)

Oh nevermind, it *does* exist already: Closed Real Interval is Compact. I would suggest extracting the part of the proof that deals with this (i.e. everything after the first paragraph) into a new proof on that page, and cross-referencing that here. --Plammens (talk) 14:40, 14 April 2021 (UTC)

Good call. But there's a reason why Sutherland goes into the details of this proof from first principles. Can't remember exactly why now, probably to do with circularity. Bear in mind that there are various contexts in which compact is defined: in the real numbers, in a metric space, in the context of topology, and all these things have to be rigorously defined as being completely identical.
The latter is the Heine-Borel Theorem, which is a complicated beast, the basis of which is Closed Bounded Subset of Real Numbers is Compact.
Also note that Closed Real Interval is Compact is currently showing "Proof 1" and "Proof 2" which arises from a fundamental misunderstanding about the philosophy of $\mathsf{Pr} \infty \mathsf{fWiki}$. Proof 1 demonstrates the result in the context of metric spaces, Proof 2 demonstrates it in the context of normed vector spaces. It has not as far as I can tell, at that stage, been proved in the context of a topological space.
If it were really that simple and trivial to "just" invoke that result, then Sutherland would have done it. The fact that he takes great pains to go through the work that Heine and Borel themselves did to make sure that compact in the context of the real number line (and general multidimensional space) means the same thing as compact in the general topological space suggests that this is necessary -- or, at the very least, instructive.
Feel free to add a simple proof, though, based on your own ideas, but be aware that it may well either be incomplete (through reliance on results that have not actually been proven) or circular (through relying on this result itself). --prime mover (talk) 15:08, 14 April 2021 (UTC)
Oh I wasn't intending to add a completely new proof, but just to refactor this page. I.e., everything after "[...] it suffices to prove that $\closedint a b$ is compact" is a proof of Closed Real Interval is Compact, but from first principles (i.e. using the general topological definition of compact). The other proofs, as you noted, use other definitions, the first one seemingly using a definition where "compact = closed & bounded" is part of the definition. My suggestion is to move the second and later paragraphs in this page into a "Proof 3" section of Closed Real Interval is Compact (or probably "promote" it to Proof 1, since it's the most general), and reference that result here to avoid duplication. This would also have the benefit of completing Closed Real Interval is Compact since right now there is no proof for the general topological definition from first principles (which is what this page has). Maybe I misunderstood what you meant? --Plammens (talk) 14:23, 15 April 2021 (UTC)
The proof itself is as it appears in Sutherland. I have issues with rewriting published proofs, the main one being that the page no longer matches the source work, and those studying that source with it open on the desk against $\mathsf{Pr} \infty \mathsf{fWiki}$ on the screen will lose track. By all means add a new proof, but it would be preferable, for all sorts of reasons, to leave this particular page here as is.
We can indeed craft that 3rd proof of Closed Real Interval is Compact, but let's get it up there now and then we can refactor the Sutherland thread to reflect what we have. --prime mover (talk) 16:30, 15 April 2021 (UTC)
Ah I see, it makes sense. Should I copy the relevant fragment verbatim (plus any necessary minor adjustments) and add the same Sutherland reference as a source? Or should it be a paraphrased/new proof? (I can paraphrase it but I don't think I can come up with a new proof.) --Plammens (talk) 15:59, 16 April 2021 (UTC)
Please feel free to extract that fragment into its own page, as you suggest -- but leave the Sutherland references alone unless a) you have an actual copy of that specific edition of the source work, and b) you are completely on board with the technique of the "prev" and "next" links (I mention this because while I believe it's fairly conceptually straightforward, editors have demonstrated in the past that it's clearly not). The result is nevertheless a good one. --prime mover (talk) 16:53, 16 April 2021 (UTC)