February 19 Information

Is there a constructive proof (i.e. a proof in constructive mathematics) of the fact that if a Cartesian product of sets is a singleton, then all of the sets are singletons? Classically, if ${\displaystyle (x_{i})_{i\in I}}$ is the unique element of the Cartesian product ${\displaystyle \prod _{i\in I}X_{i}}$, and ${\displaystyle y\in X_{i}}$, then one can consider the family ${\displaystyle (y_{j})_{j\in I}}$ where ${\displaystyle y_{i}=y}$ and ${\displaystyle y_{j}=x_{j}}$ if ${\displaystyle j\neq i}$, and from this deduce that ${\displaystyle y=x_{i}}$, showing that ${\displaystyle X_{i}}$ is a singleton for all ${\displaystyle i\in I}$. GeoffreyT2000 ( talk) 23:25, 19 February 2016 (UTC) reply

I may be missing something stupid but it seems like your proof works constructively. Let the Cartesian product be ${\displaystyle \{f\}}$ where ${\displaystyle f}$ is the tuple as a function on ${\displaystyle I}$. I'll say ${\displaystyle S}$ is a singleton if ${\displaystyle \exists x\,(S=\{x\})}$, i.e. if ${\displaystyle \exists x{\in }S\,\forall y{\in }S\,(x=y)}$. Then you want to prove ${\displaystyle \forall i{\in }I\,\exists x{\in }X_{i}\,\forall y{\in }X_{i}\,(x=y)}$. The proof is: given ${\displaystyle i}$, take ${\displaystyle x=f(i)}$; given ${\displaystyle y}$, define ${\displaystyle g(j)=(y{\mbox{ if }}j=i,f(j){\mbox{ otherwise}})}$; then ${\displaystyle g\in \{f\}}$, so ${\displaystyle g=f}$, so ${\displaystyle y=g(i)=f(i)=x}$. -- BenRG ( talk) 03:16, 22 February 2016 (UTC) reply