Talk:Sequence Characterization of Open Sets

From ProofWiki
Jump to navigation Jump to search

I get a strong sense that this result uses the Axiom of Countable Choice to find a sequence with the sought properties ("inductive definition" is basically a façade for countable choice the way it has been used here). — Lord_Farin (talk) 10:47, 26 November 2014 (UTC)

I'm not familiar with the Axiom of Countable Choice, I'm able however to fully define the sought sequence step by step using the induction principle. Might take up some space and leave the page a little messier though (at least until I adopt the established house style a little better). — Drobadur (talk) 11:08, 26 November 2014 (UTC)
The problem that you face is not with the induction an sich, but rather with the fact that you have to select an arbitrary element from a non-singleton set. Because you want to do this for all $n \in \N$, you need to use the ACC. — Lord_Farin (talk) 11:49, 26 November 2014 (UTC)
What does it say in your source work? --prime mover (talk) 19:41, 26 November 2014 (UTC)
I didn't have a source, but this math.SE reference agrees with me in quite a strong fashion. — Lord_Farin (talk) 09:56, 27 November 2014 (UTC)
Good source -- but the question was really directed to Drobadur. I'd be interested to know what (if any) etxtbook is being used as a source for this. --prime mover (talk) 14:50, 27 November 2014 (UTC)