日記2

自然演繹を積極的に用いたい．

集合の性質(定理2.5)

福田拓生『集合への入門(無限をかいま見る)』培風館 2018

定理2.5　17項

$∀x［x∈\mathbb{N}→∃x［x∈\mathbb{N}∧x=a］］$

$x=［i,j,n］_{\mathbb{N}}$ 　(∀-除去)　s.t.　 $i:=1,j:=n$

$A_1,A_2,......,A_n,B：1つの集合$

とする．このとき，次が成立する．

☆注意

このような「～とする」の意味は，もし $i=1,j=n$ であるとき次が成り立つ，という仮定の話である．

Ⅰ

(ⅰ)　 $A_j⊆\displaystyle\bigcup_{i=1}^{n}A_i$

(ⅱ)　 $\displaystyle\bigcap_{i=1}^{n}A_i⊆A_j$

Ⅱ　分配法則

(ⅰ)　 $(\bigcup_{i=1}^n A_i)∩B=\bigcup_{i=1}^n(A_i∩B)$

(ⅱ)　 $(\bigcap_{i=1}^n A_i)∪B=\bigcap_{i=1}^n(A_i∪B)$

Ⅲ

(ⅰ)　 $\displaystyle\bigcup_{i=1}^n A_i⊆B←→A_j⊆B$

(ⅱ)　 $B⊆\displaystyle\bigcap_{i=1}^n A_i←→B⊆A_j$

(証明)

Ⅰ

(ⅰ)について

$∀y［y∈A_j→∃y［y∈A_j∧y=b］］$

$x=［b］_{A_j}$ 　(∀-除去)　s.t.

$b∈A_j→b∈\displaystyle\bigcup_{i=1}^n A_i$

を示す．

1　(1)　 $b∈A_j$ 　　仮定

1　(2)　 $b∈A_1∨b∈A_2∨\cdots\cdots∨b∈A_n$ 　　1.∨-導入

i.e.　 $b∈\displaystyle\bigcup_{i=1}^n A_i$ 　　和集合の定義

　 (3)　 $b∈A_j→b∈\displaystyle\bigcup_{i=1}^n A_i$ 　　1-2.→-導入

　 (4)　 $y∈A_j→y∈\displaystyle\bigcup_{i=1}^n A_i$ 　　3.∀-導入

(ⅱ)について

$∀y［y∈\bigcap_{i=1}^n A_i→∃y［y∈\bigcap_{i=1}^n A_i∧y=b］］$

$x=［b］_{\bigcap_{i=1}^n A_i}$ 　(∀-除去)　s.t.

$b∈\displaystyle\bigcap_{i=1}^n A_i→b∈A_j$

を示す．

1　(1)　 $b∈\displaystyle\bigcap_{i=1}^n A_i$ 　　仮定

i.e.　 $b∈A_1∧b∈A_2∧\cdots\cdots∧b∈A_n$ 　　共通部分の定義

1　(2)　 $b∈A_n$ 　　1.∧-除去

i.e.　 $b∈A_j$ 　　 $(j=n)$

　 (3)　 $b∈\displaystyle\bigcap_{i=1}^n A_i→b∈A_j$ 　　1-2.→-導入

　 (4)　 $y∈\displaystyle\bigcap_{i=1}^n A_i→y∈A_j$ 　　3.∀-導入

Ⅱ

(ⅰ)

(→)について

$∀y［y∈(\bigcup_{i=1}^n A_i)∩B→∃y［y∈(\bigcup_{i=1}^n A_i)∩B∧y=b］］$

$x=［b］_{(\bigcup_{i=1}^n A_i)∩B}$ 　(∀-除去)　s.t.

$b∈(\bigcup_{i=1}^n A_i)∩B→b∈\bigcup_{i=1}^n (A_i∩B)$

を示す．

1　(1)　 $b∈(\bigcup_{i=1}^n A_i)∩B$ 　　仮定

i.e.　 $b\displaystyle\bigcup_{i=1}^n A_i∧b∈B$

i.e.　 $(b∈A_1∨b∈A_2∨\cdots\cdots∨b∈A_n)∧b∈B$

i.e.　 $(b∈A_1∧b∈B)∨(b∈A_2∧b∈B)∨\cdots\cdots∨(b∈A_n∧b∈B)$

論理的分配法則

1　 (2)　 $b∈\bigcup_{i=1}^n (A_i∩B)$ 　　1.換言

　 (3)　 $b∈(\bigcup_{i=1}^n A_i)∩B→b∈\bigcup_{i=1}^n (A_i∩B)$ 　　1-2.→-導入

　 (4)　 $y∈(\bigcup_{i=1}^n A_i)∩B→y∈\bigcup_{i=1}^n (A_i∩B)$ 　　3.∀-導入

(←)について

　(→)と同様にして論理的分配法則より成立する．(ⅱ)の(←→)も同様．

Ⅲ

(→)について

$∀z［z∈\bigcup_{i=1}^n A_i→∃z［z∈\bigcup_{i=1}^n A_i∧z=c］］$

$z=［c］_{\bigcup_{i=1}^n A_i}$ 　(∀-除去)　s.t.

$［c∈\bigcup_{i=1}^n A_i→c∈B］→［c∈A_j］$

を示す．

1　　(1)　 $c∈\displaystyle\bigcup_{i=1}^n A_i→c∈B$ 　　仮定

2　　(2)　 $c∈\displaystyle\bigcup_{i=1}^n A_i$ 　　仮定

i.e.　 $c∈A_1∨c∈A_2∨\cdots\cdots∨c∈A_n$

3　　(3)　 $c∈A_n$ 　　仮定

1,3　 (4)　 $c∈B$ 　　1,3.→-除去

1　　(5)　 $c∈A_n→c∈B$ 　　3-4.→-導入

　　 (6)　 $c∈A_j→c∈B$ 　　2-5.∨-除去

　　 (7)　 $［c∈\displaystyle\bigcup_{i=1}^n A_i→c∈B］$

$→［c∈A_j→c∈B］$ 　　1-5.→-導入

　　 (8)　 $［z∈\displaystyle\bigcup_{i=1}^n A_i→z∈B］$

$→［z∈A_j→z∈B］$ 　　7.-導入

以下同様．▢