book プレビュー

6 自然数の補足

word(ss,s) … \(+\)
^*+. … \([+] \stackrel{\star\!\star}{=} \; [\stackrel{\text{^*}}{+}]\)

6.1 順序

word(ss,p) … \(\le\) \(<\)
≤. … \(m , n \in \mathbb{M} \Longrightarrow ( m \le n \Longleftrightarrow \exists k \in \mathbb{M} . m + k = n )\)
<. … \(m < n \Longleftrightarrow m \le n , m \neq n\)
L+c … \(x , y , k \in \mathbb{M} , x + k = y + k \Longrightarrow x = y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L+0 … \(m , k \in \mathbb{M} , m + k = m \Longrightarrow k = 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L+1+ … \(j , m \in \mathbb{M} \Longrightarrow ( j + 1 ) + m = ( j + m ) + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L<+1 … \(m , n \in \mathbb{M} \Longrightarrow ( m < n \Longleftrightarrow m + 1 \le n )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L<≤ … \(m , n \in \mathbb{M} , m \le n \Longrightarrow \neg n < m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L≤R … \(n \in \mathbb{M} \Longrightarrow n \le n , \neg n + 1 \le n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L≤+1 … \(x , n \in \mathbb{M} , x \le n \Longrightarrow x \le n + 1 , x \neq n + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
Ltot … \(m , n \in \mathbb{M} \Longrightarrow m \le n \mathbin{\rm o\!r} n < m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L≤s … \(i , n \in \mathbb{M} \Longrightarrow ( i \le n + 1 \Longleftrightarrow i \le n \mathbin{\rm o\!r} i = n + 1 )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L0≤ … \(k \in \mathbb{M} \Longrightarrow 0 \le k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L≤tr … \(m , n , p \in \mathbb{M} , m \le n \le p \Longrightarrow m \le p\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L<A … \(x , y \in \mathbb{M} , x < y \Longrightarrow \neg y < x , x \le y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L≤< … \(a , b \in \mathbb{M} , a \le b \Longrightarrow a = b \mathbin{\rm o\!r} a < b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L<s … \(n \in \mathbb{M} \Longrightarrow n < n + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L<s≤ … \(z , b \in \mathbb{M} , z < b + 1 \Longrightarrow z \le b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L<0 … \(z \in \mathbb{M} \Longrightarrow \neg z < 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
L<+k … \(k , d \in \mathbb{M} , k \neq 0 \Longrightarrow d < d + k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
強い帰納法：\(n\) より小さいすべてで成り立てば \(n\) でも成り立つなら、すべての \(n\) で成り立つ（SIND）。
SIND … \(\forall n \in \mathbb{M} . ( \forall z \in \mathbb{M} . ( z < n \Longrightarrow z \in E ) \Longrightarrow n \in E ) , n \in \mathbb{M} \Longrightarrow n \in E\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄
⋅K … \(x , y \in \mathbb{M} , a \in \mathbb{N} , x \cdot a = y \cdot a \Longrightarrow x = y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄

6.2 偶数と奇数

どの自然数も偶数 \(2k\) か奇数 \(2k+1\) のどちらか一方（Lpar・Lodd）。
Lpar … \(m \in \mathbb{M} \Longrightarrow \exists k \in \mathbb{M} . m = 2 \cdot k \mathbin{\rm o\!r} m = 2 \cdot k + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
N1 … \(a \in \mathbb{M} \Longrightarrow 2 \cdot ( a + 1 ) = ( 2 \cdot a + 1 ) + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lodd … \(a , b \in \mathbb{M} \Longrightarrow 2 \cdot a \neq 2 \cdot b + 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄

6.3 整除と素数

word(ss,p) … \(\mid\)
∣. … \(d \mid n \Longleftrightarrow \exists k \in \mathbb{M} . n = d \cdot k\)
∣≤ … \(d \in \mathbb{M} , n \in \mathbb{N} , d \mid n \Longrightarrow d \le n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
∣T … \(p , d , n \in \mathbb{M} , p \mid d , d \mid n \Longrightarrow p \mid n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
∣+ … \(d , a , b \in \mathbb{M} , d \mid a , d \mid b \Longrightarrow d \mid a + b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
∣sub … \(d , u , v \in \mathbb{M} , d \mid u + v , d \mid u \Longrightarrow d \mid v\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
word(,s) … \(\mathbb{P}\)
ℙ. … \(\mathbb{P} = \{ p \in \mathbb{N} \mid 2 \le p , \forall d \in \mathbb{N} . ( d \mid p \Longrightarrow d = 1 \mathbin{\rm o\!r} d = p ) \}\)

6.4 区間

6.5 値ごとに分けて数える

\(S\) の各元に \(Y\) の元 \(a\) が1つずつ対応し（\(R\)）、\(a\) に対応する元がちょうど \(g(a)\) 個なら、\(S\) は \(\{(a, j) \mid a \in Y, j \in g(a)\}\) と個数が等しい（Mathlib の card_eq_sum_card_fiberwise）。\(a\) を1つ除いた場合から帰納法で示す。
どの値の部分もちょうど \(q\) 個なら、\(S\) は \(q \cdot k\) 個（\(Y\) は \(k\) 個）。
LΣc … \(Y \stackrel{\#}= k \in \mathbb{M} , R \subset S \times Y , \forall s \in S . \exists! e \, \langle s , e \rangle \in R , q \in \mathbb{M} , \forall e \in Y . \forall G \, ( \forall s \, ( s \in G \Longleftrightarrow \langle s , e \rangle \in R ) \Longrightarrow G \stackrel{\#}= q ) \Longrightarrow S \stackrel{\#}= q \cdot k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄

6.6 階乗と組合せ

LFib … \(z \in X , a \in Y , \forall f \, ( f \in F \Longleftrightarrow f \in X \stackrel{\rm IS}\to Y , \langle z , a \rangle \in f ) \Longrightarrow F \stackrel{\#}= X \mathop\setminus \{ z \} \stackrel{\rm IS}\to Y \mathop\setminus \{ a \}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
LIS … \(k \in \mathbb{M} , \forall U , V \, ( U \stackrel{\#}= k , V \stackrel{\#}= k \Longrightarrow U \stackrel{\rm IS}\to V \stackrel{\#}= k ! ) , X \stackrel{\#}= k + 1 , Y \stackrel{\#}= k + 1 , z \in X \Longrightarrow X \stackrel{\rm IS}\to Y \stackrel{\#}= k ! \cdot ( k + 1 )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，!𝕄
→IS=#! … \(n \in \mathbb{M} \Longrightarrow \forall U , V \, ( U \stackrel{\#}= n , V \stackrel{\#}= n \Longrightarrow U \stackrel{\rm IS}\to V \stackrel{\#}= n ! )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，!𝕄
word(ss,s) … \(\mathrm{C}\)
AxC … \(n , k \in \mathbb{M} \Longrightarrow n \mathrm{C} k \in \mathbb{M} , n \mathrm{C} k \stackrel{\#}= \{ A \in \wp n \mid A \stackrel{\#}= k \}\)
L*# … \(A \subset X , h \in X \stackrel{\rm IS}\to Y \Longrightarrow A \stackrel{\#}= h ( A )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s
choose=# … \(X \stackrel{\#}= n \in \mathbb{M} , k \in \mathbb{M} \Longrightarrow n \mathrm{C} k \in \mathbb{M} , \exists S \, \forall A \, ( A \in S \Longleftrightarrow A \subset X , A \stackrel{\#}= k ) , S \stackrel{\#}= n \mathrm{C} k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，AxC
0 元部分集合は空集合だけ。
LC0 … \(n \in \mathbb{M} \Longrightarrow n \mathrm{C} 0 = 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxC

6.7 和

word(s,s) … \(\sum\)
abbr … \(\sum_{ x \in Y } X\) ≈ \(\sum ( \lceil x \mapsto X \rfloor | _ Y )\)
和 \(\sum f\) は、空の写像で 0、1点 \(\langle x, y\rangle\) を足すと \(y\) が足される（AxΣ）。値の範囲は問わない。
AxΣ … \(\begin{cases} \sum \emptyset = 0 \\ X \stackrel{\#}= k \in \mathbb{M} , f \in X \to V , x \notin X \Longrightarrow \sum ( f \cup \{ \langle x , y \rangle \} ) = \sum f + y \end{cases}\)
値が自然数なら、\(\sum f\) は \(f(x)\) 個ずつ並べた集合の個数（Σ=#）。
Σ=# … \(X \stackrel{\#}= k \in \mathbb{M} , f \in X \to \mathbb{M} \Longrightarrow \sum f \in \mathbb{M} , \exists U \, \forall q \, ( q \in U \Longleftrightarrow \exists c , z , j \, \langle c , z \rangle \in f , j \in z , q = \langle c , j \rangle ) , U \stackrel{\#}= \sum f\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxΣ
1点だけの和はその値。
L∑1 … \(y \in \mathbb{M} , \forall p \, ( p \in f \Longleftrightarrow p = \langle x , y \rangle ) \Longrightarrow \sum f = y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxΣ
1点だけの和は、加法の単位元 0 をもつ集合 \(S\) の上ではその値。
L∑1S … \(0 \in \text{unit} ( S , [+] ) , y \in S , \forall p \, ( p \in f \Longleftrightarrow p = \langle x , y \rangle ) \Longrightarrow \sum f = y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxΣ
区間 \(0 .. n\) の和に \(n + 1\) の項を足す。
L∑..s … \(n \in \mathbb{M} , g \in 0 \mathinner{\ldotp\ldotp} n \to V , \forall p \, ( p \in f \Longleftrightarrow p \in g \mathbin{\rm o\!r} p = \langle ( n + 1 ) , y \rangle ) \Longrightarrow \sum f = \sum g + y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxΣ
値 \(e\) の部分がちょうど \(g(e)\) 個なら、\(S\) は \(\sum g\) 個。
LΣ∑ … \(Y \stackrel{\#}= k \in \mathbb{M} , R \subset S \times Y , \forall s \in S . \exists! e \, \langle s , e \rangle \in R , g \in Y \to \mathbb{M} , \forall e , w \, ( \langle e , w \rangle \in g \Longrightarrow \forall F \, ( \forall s \, ( s \in F \Longleftrightarrow \langle s , e \rangle \in R ) \Longrightarrow F \stackrel{\#}= w ) ) \Longrightarrow \sum g \in \mathbb{M} , S \stackrel{\#}= \sum g\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxΣ