Talk:Union from Synthetic Basis is Topology/Proof 1

From ProofWiki
Jump to navigation Jump to search

"AC is used". I presume one means that we have to choose a particular representation of any set in $\vartheta$? It sounds like it could be that AC is used here, indeed. But I suspect also that $\vartheta$ could be characterised in a more cumbersome way, thus maybe avoiding AC. This is worth some thought. --Lord_Farin (talk) 09:50, 24 September 2012 (UTC)

On this matter, could it be that one could write:

$U = \bigcup \left\{{B \in \mathcal B: B \subseteq U}\right\}$

which apparently avoids the use of a choice function? Of course, the proof will have to be changed to use this construction, but I think that the parts $(2)$ and $(3)$ can be shown using this language - a bit cumbersome, but avoiding AC makes it worthwhile. --Lord_Farin (talk) 09:57, 24 September 2012 (UTC)

Yeah, that resolves the issue. Thanks. --abcxyz (talk) 20:05, 25 September 2012 (UTC)
I have applied above construction; it worked. I am quite sure I didn't use AC in the new proof, but please read it to ensure it is not essentially flawed. I have glossed over some applications of a theorem saying:
$\mathbb S \subseteq \mathbb T \implies \bigcup \mathbb S \subseteq \bigcup \mathbb T$
which I didn't manage to locate. --Lord_Farin (talk) 12:01, 24 September 2012 (UTC)

Axeman cometh

Bizarre. A carefully constructed proof is axed down to practically nothing. Get a grip, gentlemen! --prime mover (talk) 21:06, 25 September 2012 (UTC)

I am quite, well, almost offended by the recent edits; significantly, that the point that a union of unions is not a union (but only equal to a different union), which I carefully acknowledged in my (admittedly long and imperfect) proof has been glossed over in favour of what was in place before I overcame the use of AC in the proof, only augmented by some fancy symbols in place of words. Reword the proof if necessary, even scrap parts of it; but please *do* ensure that the standard of rigour is not compromised in the process. --Lord_Farin (talk) 22:19, 25 September 2012 (UTC)
Maybe we could create a page proving that:
$\ds \bigcup_{i \mathop \in I} \bigcup \Bbb S_i = \bigcup \bigcup_{i \mathop \in I} \Bbb S_i = \bigcup \left\{{S: \exists i \in I: S \in \Bbb S_i}\right\}$
and just use that fact in the proofs of $\left({1}\right)$ and $\left({2}\right)$? Any comments? --abcxyz (talk) 14:45, 26 September 2012 (UTC)
Now you're starting to get the hang of this site. --prime mover (talk) 18:46, 26 September 2012 (UTC)
Okay, I think I see your point. Sorry. I've changed it. What do you think? --abcxyz (talk) 23:29, 25 September 2012 (UTC)
My view is that it would be best to put each of the separate parts of the proof be placed into its own page as separate proofs in their own right. Then the combined proof can be accomplished by linking to these rather more fundamental results. In that way it will be easier to put multiple proofs together of the apparently-contentious part 2 (and to a lesser extent part 3) in the standard house style of transclusion into those separate pages. --prime mover (talk) 06:07, 26 September 2012 (UTC)
Better now, thanks; no offense taken as you have displayed eagerness to learn. I think the Union of Unions result is a good idea. With reference to that, I think we can cut some trees in $(2)$ and $(3)$. Not sure about transclusion, though, unless there are alternatives for only a certain part. Also it stands as an open task to separate theorem and definition here. --Lord_Farin (talk) 22:16, 26 September 2012 (UTC)
Transclusion, as I envisaged it, would happen only if there were more than one proof for a separate subpart of this proof here, those individual subparts would be configured with the same technique used for multiple proofs currently. --prime mover (talk) 05:17, 27 September 2012 (UTC)