\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{Cantor's theorem} \hypertarget{cantors_theorem}{}\section*{{Cantor's Theorem}}\label{cantors_theorem} \noindent\hyperlink{summary}{Summary}\dotfill \pageref*{summary} \linebreak \noindent\hyperlink{history}{History}\dotfill \pageref*{history} \linebreak \noindent\hyperlink{statements_and_proofs}{Statements and proofs}\dotfill \pageref*{statements_and_proofs} \linebreak \noindent\hyperlink{interpretation}{Interpretation}\dotfill \pageref*{interpretation} \linebreak \noindent\hyperlink{in_posets}{In posets}\dotfill \pageref*{in_posets} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{summary}{}\subsection*{{Summary}}\label{summary} [[Georg Cantor]] proved many theorems, but the one usually called \emph{Cantor's theorem} is the first nontrivial theorem of Cantor's new [[set theory]]: that some infinities are bigger than others; in particular, any infinite [[cardinal number]] (or [[infinite set]]) generates a larger one by taking the [[power set]]. (The theorem applies to all sets, not just infinite ones, although it's fairly obvious for [[finite sets]].) Cantor's theorem should not be confused with the Cantor--Schroeder--Bernstein theorem (see [[cardinal number]]), which is different (but related, as it is important to justify Cantor's interpretation of his theorem). \hypertarget{history}{}\subsection*{{History}}\label{history} Prior to Cantor, people tended to think of infinity (whether they believed in it or not) as an absolute concept: all infinities are equivalent. It had been noticed (by [[Galileo Galilei|Galileo]], for example) that it's possible to give an [[infinite set]] a [[self-function|self]]-[[injection]] that is not a [[surjection]]; for example, the inclusion of the even integers into the integers by doubling. Thus here are two infinities ---the infinity $E$ of even integers and the infinity $N$ of all integers--- that are actually equivalent, even though at first glance it would appear that $E$ is smaller. Cantor showed that such an equivalence \emph{fails} with the [[real numbers]] $R$: no map from $N$ to $R$ can be surjective (so that $R$ is [[uncountable set|uncountable]]). His first argument was ad hoc, but he then generalised this with the \emph{diagonal argument} to show that no map from any set $S$ to its [[power set]] $\mathcal{P}S$ could be surjective. (This covered the uncountability of $R$, since Cantor found a [[bijection]] between $R$ and $\mathcal{P}N$, which we can now regard as an instance of the [[Cantor–Schröder–Bernstein Theorem]].) As there is an obvious injective map (the [[singleton]] map) from $S$ to $\mathcal{P}S$, Cantor concluded that the cardinality of the one is strictly smaller than the cardinality of the other. Cantor's argument, like his whole set theory, was controversial at the time. Those who, like [[Leopold Kronecker|Kronecker]], believed that all mathematics should be [[finite mathematics]], considered it meaningless. Even more moderate early [[constructive mathematics|constructivists]], such as [[Jan Brouwer|Brouwer]] and [[Hermann Weyl|Weyl]], found that it had little point. (In particular, it says nothing directly about $R$, since the bijection between $R$ and $\mathcal{P}N$ is not constructively valid, although Cantor's original proof that $R$ is uncountable can be made to work.) However, the versions of the theorem stated below are constructively valid, and Theorem \ref{lawvere} is even [[predicative mathematics|predicatively]] valid (as long as one has [[function sets]]); modern constructivists generally accept these as theorems. (The interpretation, however, is not so clear.) They are in fact theorems in the [[internal logic|internal language]] of any [[topos]] (and Theorem \ref{lawvere} is a theorem in any $\Pi$-[[pretopos]]). \hypertarget{statements_and_proofs}{}\subsection*{{Statements and proofs}}\label{statements_and_proofs} \begin{theorem} \label{lawvere}\hypertarget{lawvere}{} (Lawvere's version.) Given sets $S$ and $V$, suppose that there is a [[surjection]] from $S$ to the [[function set]] $S \to V$ (also written $V^S$). Then every map $n\colon V \to V$ has a [[fixed point]]; that is, $n(x) = x$ for some $x\colon V$. \end{theorem} (This generalizes to \emph{[[Lawvere's fixed point theorem]]}.) \begin{proof} Let $f\colon S \to (S \to V)$ be any function, and consider the function $g\colon S \to V$ given by \begin{displaymath} g(a) = n(f(a)(a)) . \end{displaymath} That is, if one uses [[currying]] to interpret $f$ as a function from $S \times S$ to $V$, then $g$ is defined using the [[diagonal map]] $\Delta_S$ as \begin{displaymath} S \stackrel{\Delta_S}\to S \times S \stackrel{f}\to V \stackrel{n}\to V . \end{displaymath} Now suppose that $f$ is surjective. Then there must be some element $a\colon S$ such that $f(a) = g$. But then \begin{displaymath} g(a) = n(f(a)(a)) = n(g(a)) , \end{displaymath} so $g(a)$ is a fixed point of $n$. \end{proof} The presence of the diagonal map $\Delta_S$ here explains why this proof is called the \emph{diagonal argument}. (This explanation is anachronistic but morally correct.) Lawvere's proof also explains (in fact generalizes) the $Y$ or [[fixed-point combinator]] in [[untyped lambda-calculus]], where $Y(n)$ is a fixed-point for any term $n$. It immediately follows (even constructively) that if $V$ has a [[self-mapping]] with no fixed point, then no map from $S$ to $S \to V$ can be a surjection. In fact, we have something slightly stronger than (but classically equivalent to) the failure of $f$ to be a surjection: there actually exists an element $g$ of $S \to V$ that is not equal to any value in the range of $f$. (If $V$ has an [[apartness relation]], then you can get an even stronger result for a correspondingly stronger hypothesis on $n$, but that doesn't apply to the versions below.) \begin{theorem} \label{cantor}\hypertarget{cantor}{} (Cantor's version.) Given a set $S$, there is no surjection from $S$ to the [[power set]] $\mathcal{P}S$. \end{theorem} \begin{proof} Let $V$ be the set of [[truth values]], and let $n\colon V \to V$ be [[negation]]. Since $n$ has no fixed point, apply Theorem \ref{lawvere}. \end{proof} Note that although negation doesn't have all of its usual properties in constructive mathematics, $p = \neg{p}$ is still impossible. The next version is classically equivalent to the previous version (at least if you check that $\mathcal{P}S$ is [[inhabited set|inhabited]]), but not constructively equivalent. (Indeed, unlike Theorem \ref{lawvere}, it apparently has no constructive analogue when $\mathcal{P}S$ is replaced by $V^S$.) This argument is from Proposition 2.8.8 of Taylor's \emph{[[Practical Foundations]]} (although I don't know if it really originated there). \begin{theorem} \label{taylor}\hypertarget{taylor}{} (Taylor's version.) Given a set $S$, there is no [[injection]] from $\mathcal{P}S$ to $S$. \end{theorem} \begin{proof} Let $i\colon \mathcal{P}S \to S$ be any function. Define $f\colon S \to \mathcal{P}S$ as follows: \begin{displaymath} f(a) = \{ b\colon S \;|\; \forall (U\colon \mathcal{P}S),\; i(U) = a \;\Rightarrow\; b \in U \} . \end{displaymath} If $i$ is an injection, then $f$ is a [[retraction]] of $i$ and hence a surjection, which is impossible by Theorem \ref{cantor}. \end{proof} Of course, Cantor also proved Theorem \ref{taylor}, but his proof was not constructive. We can combine Theorems \ref{cantor} and \ref{taylor} into the following even more general statement, taken from D4.1.8 of Johnstone's \emph{[[Elephant]]}. \begin{theorem} \label{johnstone}\hypertarget{johnstone}{} (Johnstone's version.) Given a set $S$, its power set $\mathcal{P}S$ cannot be expressed as a [[subquotient]] of $S$. \end{theorem} \begin{proof} Suppose we had a set $B$, an injection $i\colon B \hookrightarrow S$ and a surjection $f\colon B \to \mathcal{P}S$. Then the [[preimage]] function $i^*\colon\mathcal{P}S \to \mathcal{P}B$ would be a surjection (because $i^\ast \exists_i = 1_{\mathcal{P}B}$), as would the [[image]] function $\exists_f\colon \mathcal{P}B \to \mathcal{P}\mathcal{P}S$ (because $\exists_f f^\ast = 1_{\mathcal{P}\mathcal{P}S}$). Thus their composite would be a surjection $\mathcal{P}S \to \mathcal{P}\mathcal{P}S$, which is impossible by Theorem \ref{cantor}. \end{proof} \hypertarget{interpretation}{}\subsection*{{Interpretation}}\label{interpretation} Note that there exists an [[injection]] from $S$ to $\mathcal{P}S$, given by the [[singleton]] map. So in the arithmetic of [[cardinal numbers]], we have \begin{displaymath} {|S|} \leq {|\mathcal{P}S|} . \end{displaymath} But as there is no such surjection, there certainly is no [[bijection]], and we have \begin{displaymath} {|S|} \ne {|\mathcal{P}S|} . \end{displaymath} So we conclude that \begin{displaymath} {|S|} \lt {|\mathcal{P}S|} . \end{displaymath} That is, each set is strictly smaller in cardinality than its power set. This interpretation relies on a good relationship between $\leq$ and $=$ on the class of cardinal numbers; in particular, the Cantor--Schroeder--Bernstein theorem that $\leq$ is [[antisymmetric relation|antisymmetric]]. In [[constructive mathematics]], this relationship is lacking, and it is quite possible for two sets to each be strictly smaller than each other in the sense above. Thanks to Theorem \ref{taylor}, this is not possible for a set and its power set, but it does mean that the interpretation of $\lt$ as relative size is problematic ---indeed almost as problematic as the idea that there are fewer even integers than integers! [[Paul Taylor]] has argued that the essential value of Cantor's Theorem is the lemma, implicit in Cantor's proof, that [[Bill Lawvere]] isolated as Theorem \ref{lawvere}. As the main interpretation of Theorem \ref{cantor} is meaningful only in a specific set-theoretic context (particularly, one where the Cantor--Schroeder--Bernstein theorem holds), it may not survive a `revolution' that overthrows the primacy of that context. But Lawvere's lemma will survive, since it `does the work' while Cantor's theorem `takes the credit'. (See \hyperlink{Taylor2009}{Taylor 2009} below for further discussion of `Lemmas that do the work and Theorems that take the credit'.) \hypertarget{in_posets}{}\subsection*{{In posets}}\label{in_posets} A theorem analogous to Cantor's theorem for sets can be formulated for other [[cartesian closed categories]]. In particular, one may ask whether it is possible to have a surjection $X \to 2^X$ between posets, where the base $2$ is not the discrete poset $\{0, 1\}$ but rather the order $\{0 \leq 1\}$. The answer is there is no such surjection $f: X \to 2^X$, but this does not follow from a simple application of Lawvere's fixed-point theorem, where one tries to rule out such $f$ by invoking existence of a map $2 \to 2$ that has no [[fixed point]] (there is no such poset map $2 \to 2$!). Nor can we appeal to some crude cardinality argument; for example, if $X$ is the ordinal $\omega$, then $2^X$ is the order $\bot \sqcup \omega^{op}$ (freely adjoin a bottom element $\bot$ to $\omega^{op}$), which has the same cardinality. So some other proof must be sought. Proving there is no surjection $X \to 2^X$ is an amusing exercise. One line of attack (which internalizes to any topos) may be found \href{https://ncatlab.org/toddtrimble/published/Cantor's+theorem+for+posets}{here}. \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[Lawvere's fixed point theorem]] \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item Taylor 2009 June 20: On the categories mailing list, Message-ID \href{http://www.mta.ca/~cat-dist/archive/2009/09-6}{E1MJ5TV-00066b-BI@mailserv.mta.ca}. \item On constructivenews, a \href{https://groups.google.com/group/constructivenews/browse_thread/thread/5f65c7ac479c15dd}{discussion} about Theorem \ref{taylor} in the case where $S$ and $V$ are both the set of [[natural numbers]]. (Apparently this fails in certain [[realizability topos]]es.) \end{itemize} [[!redirects Cantor theorem]] [[!redirects Cantor Theorem]] [[!redirects Cantor's theorem]] [[!redirects Cantor's Theorem]] [[!redirects Cantor's theorem]] [[!redirects Cantor's Theorem]] [[!redirects cantor theorem]] [[!redirects cantor Theorem]] [[!redirects cantor's theorem]] [[!redirects cantor's Theorem]] [[!redirects cantor's theorem]] [[!redirects cantor's Theorem]] \end{document}