Why does one say 'finitary'? Surely we just mean 'discrete analogues' in this case?

Indeed I have. I'm not claiming that what I've written is a proof. But the idea of the proof I've alluded to is an example of an application of the idea of connectedness.

Indeed Michael. I am not one to worry about the axiom of choice usually (i.e. it's use wasn't my main point) and probably as a result of this I do remember a struggle with some friends to find where we had used full choice in said proof, since it was just one word: blah blah blah ....then F converges to x, say......

[My previous is in response to Pierre's]

I think perhaps it's more accurate to say that the ultrafilters hide the details of the Loomis proof. The fiddling around with FIP and Zorn's and what not goes into setting up ultrafilters and characterizing compactness, after which the proof is two-three lines long.

Yes. I can't say I know lots of proofs of Tychonoff's, but I think that the ultrafilter proof is very nice indeed. Property 2. you mention seems to show very clearly how they are a useful generalization of sequences.

Any chance you could please just give extra clarification as to where the $m$'s come from? Many thanks.

Does this arguement avoid assuming that the boundary of the set is of measure zero? I might be overcomplicating things but it's something that worried me last time I thought about the problem.

Well, those functions in $L^2$ all of whose weak first derivatives are given by $L^2$ functions.

For those of us who are not so well versed in these matters but curious nevertheless, what is the L(R) which appears here?

This might just be my favourite MO Q.