有限集合
受験関係ないやろ
定義takker.icon
記号はtakker.iconが独自に作った
$ A\lesssim_\# B:\iff\exist f:A\rightarrowtail B
$ A\gtrsim_\#B:\iff\exist f:A\twoheadrightarrow B
$ A\sim_\#B:\iff\exist f:A⤖B
証明
$ Aが高々可算集合$ \iff A\lesssim_\#\Nと表せる？ 補題6.1$ \forall m,n\in\Z_{\ge0}:
1. $ \N_{\le m}\lesssim_\#N_{\le n}\implies m\le n
2. $ \N_{\le m}\gtrsim_\#\N_{\le n}\implies m\ge n
3. $ \N_{\le m}\sim_\#\N_{\le n}\implies m=n
1,2から示せる
定理6.2
$ \forall A\forall m,n\in\Z_{\ge0}:
$ \begin{dcases}\N_{\le m}\sim_\#A\\\N_{\le n}\sim_\#A\end{dcases}\implies m=n
証明：$ \forall A\forall m,n\in\Z_{\ge0}:
$ \begin{dcases}\N_{\le m}\sim_\#A\\\N_{\le n}\sim_\#A\end{dcases}
$ \iff\exist f:\N_{\le m}⤖A\exist g:\N_{\le n}⤖A
$ \iff\exist f:\N_{\le m}⤖A\exist g:\N_{\le n}⤖A:f\circ g^{-1}:\N_{\le m}⤖\N_{\le n}
$ \implies\exist h:\N_{\le m}⤖\N_{\le n}
$ \underline{\iff m=n\quad}_\blacksquare
定義6.3$ \forall A:
$ Aが有限集合である$ :\iff\exist n\in\Z_{\ge0}:\N_{\le n}\sim_\#A 定理6.2より$ nが存在すれば一意なので、これを$ |A|で表す
$ (\exist n\in\N:A\sim_\#\N_{\le n}) \iff A<_\#\N だと便利だが、選択公理が必要みたいtakker.icon 定義6.4$ \forall A：$ Aは無限集合である$ :\iff\lnot($ Aは有限集合である) 定理6.5$ \forall n\in\Z_{\ge0};|\N_{\le n}|=n
定理6.6$ \forall A:A=\varnothing\iff|A|=0
定理6.7$ \forall A,B:A,Bが有限集合$ \implies(|A|=|B|\iff A\sim_\#B) 定理6.8$ \forall A,B:Aが有限集合$ \land A\sim_\#B\implies Bは有限集合 定理6.9$ \forall A,B:A,Bが有限集合$ \implies(|A|\le|B|\iff A\lesssim_\# B) 補題6.10$ \forall n\in\Z_{\ge0}\forall A\subseteq\N_{\le n}:Aは有限集合$ \land|A|\le n 定理6.11
$ \forall A,B:A,Bが有限集合$ \land A\subseteq B\implies|A|\le|B| 定理7.3$ \forall A,B\forall f:A\rightarrowtail B:A\sim_\#f^\to(A)
補題7.7 $ \forall A:A\sim_\#\N\implies\forall B\subseteq A:Bは無限集合$ \implies B\sim_\#\N
定理7.19$ \Bbb{Q}\sim_\#\N
補題9.4 推移律$ \forall A,B,C:A\lesssim_\#B\lesssim_\#C\implies A\lesssim_\#C 補題9.5$ \lnot\exist A:2^A\lesssim_\# A
定理9.6$ \forall A:A<_\#2^A
$ <_\#：単射は存在するが全射は存在しない
$ \forall A,B:A\lesssim_\#B\lesssim_\#A\implies A\sim_\#B
定理9.13$ \forall n\in\N:\R^n\sim_\#\R
$ \forall X\neq\varnothing\forall Y:X\lesssim_\# Y\implies Y\gtrsim_\# X
$ X\neq\varnothing\iff\exist x_0:x_0\in Xと変形し、この$ x_0を用いる
$ fは単射なので、$ f':X\ni x\mapsto f(x)\in f^\to(X)とすると、$ f'は全単射になる。ここで$ fの$ Xによる像を$ f^\to(X)とした
$ g:Y\ni y\mapsto\begin{dcases}{f'}^{-1}(y)&\text{if }y\in f^\to(X)\\x_0&\text{otherwise}\end{dcases}\in Xが全射になることを示せばいい
このとき$ {f'}^{-1}の全射性より$ \forall x\in X\exist y\in f^\to(X):{f'}^{-1}(y)=xとなり、$ \forall x\in X\exist y\in Y:h(y)=xだから$ hは全射である