未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
articles3/31.book
ヘッダ
行番号
title Ramsey の定理 import 0-pa formel /common/default thmel /common/zf option review quick:true;
section 準備 word ap txt 列 \(f\) の1点の値だけを変えた列があること（upd𝕄・73 と同じ）を仮定します。 prop upd𝕄 <- `[ ∃ g \, (g ap (k) = p and [ ∀ i ∈ 𝕄 . (i {/}= k ⟹ g ap (i) = f ap (i)) ]) ]` txt 長さ \(P\) の有限列を対 \(\langle x,P\rangle\) で表します。\(x \upuparrows P\)：増加列。\(\langle x,P\rangle \sqsubseteq \langle v,L\rangle\)：\(x\) の値はどれも \(v\) の値。\(c \models_0 \langle x,P\rangle\)：色付け \(c\) で \(x\) のどの2点も赤（値 0）。\(\models_1\) は青（値 \(\ne 0\)）。 word \pr abbr pr word ⇈ ⊑ ⊨₀ ⊨₁ prop ⇈. <- `x ⇈ P ⟺ [ ∀ i ∈ 𝕄 . (i < P ⟹ x ap (i) ∈ 𝕄) ] and [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < j and j < P ⟹ x ap (i) < x ap (j)) ] ]` prop ⊑. <- `\< pr x ; P \> ⊑ \< pr v ; L \> ⟺ [ ∀ i ∈ 𝕄 . (i < P ⟹ [ ∃ j ∈ 𝕄 . j < L and x ap (i) = v ap (j) ]) ]` prop ⊨₀. <- `c ⊨₀ \< pr x ; P \> ⟺ [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < j and j < P ⟹ (c ap (x ap (i))) ap (x ap (j)) = 0) ] ]` prop ⊨₁. <- `c ⊨₁ \< pr x ; P \> ⟺ [ ∀ i ∈ 𝕄 . [ ∀ j ∈ 𝕄 . (i < j and j < P ⟹ (c ap (x ap (i))) ap (x ap (j)) {/}= 0) ] ]` let/thm R0Q <- `Q ∈ 𝕄 ⟹ [ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and 0 ≤ L ⟹ [ ∃ x \, ((x ⇈ 0 and \< pr x ; 0 \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; 0 \>) or (x ⇈ Q and \< pr x ; Q \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; Q \>)) ]) ] ] ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 prf R0Q / W. -| L<0 , 𝕄0s v; R0Q -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 h; let/thm RP0 <- `P ∈ 𝕄 ⟹ [ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and 0 ≤ L ⟹ [ ∃ x \, ((x ⇈ P and \< pr x ; P \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; P \>) or (x ⇈ 0 and \< pr x ; 0 \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; 0 \>)) ]) ] ] ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 prf RP0 / W. -| L<0 , 𝕄0s v; RP0 -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 h; let/thm Lsplit <- `[ a ; b ; n ; m col ∈ 𝕄 ] and n + m ≤ a + b ⟹ n ≤ a or m ≤ b` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , 1. prf A1 <- `[ x ; y ; z ; w col ∈ 𝕄 ] and x ≤ y and z ≤ w ⟹ x + z ≤ y + w` / ≤. -| +A , +C , +∈𝕄 v; A2 <- `[ a ; b col ∈ 𝕄 ] ⟹ (a + b) suc ≤ a suc + b suc` / ≤. -| Lsuc+ , +𝕄 , +1 , +C , +∈𝕄 , 1. , 𝕄0s v; B1 <- `[ a ; b ; n ; m col ∈ 𝕄 ] and a suc ≤ n and b suc ≤ m ⟹ (a + b) suc ≤ n + m` -| A1 , A2 , L≤T , +∈𝕄 , 𝕄0s v; Lsplit -| Ltot / <. , B1 , L≤T , L<irr / <. , +∈𝕄 , 𝕄0s v; Lsplit -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , 1. h; section 数える txt 最後の頂点 \(v(m)\) より前の頂点を、\(v(m)\) と赤で結ばれるものの列 \(r\) と青で結ばれるものの列 \(u\) に振り分けます（ENUM）。 let/thm ENUM <- `[ m ; M col ∈ 𝕄 ] and v ⇈ m suc and M ≤ m ⟹ [ ∃ a ∈ 𝕄 . [ ∃ b ∈ 𝕄 . a + b = M and [ ∃ r \, (r ⇈ a and \< pr r ; a \> ⊑ \< pr v ; M \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (c ap (r ap (i))) ap (v ap (m)) = 0) ]) ] and [ ∃ u \, (u ⇈ b and \< pr u ; b \> ⊑ \< pr v ; M \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (c ap (u ap (i))) ap (v ap (m)) {/}= 0) ]) ] ] ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , upd𝕄 prf hym <- `|m ∈ 𝕄` ; hyM <- `|M ∈ 𝕄 and |M ≤ |m` ; hyV <- `|v ⇈ |m suc` ; E0 <- `[ ∃ a ∈ 𝕄 . [ ∃ b ∈ 𝕄 . a + b = 0 and [ ∃ r \, (r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; 0 \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ]) ] and [ ∃ u \, (u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; 0 \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ]) ] ] ]` / ⇈. / ⊑. -| L<0 , L0+ , 𝕄0s v; KS <- `M ∈ 𝕄 and \< pr r ; a \> ⊑ \< pr |v ; M \> ⟹ \< pr r ; a \> ⊑ \< pr |v ; M suc \>` / ⊑. -| L<K p; XR <- `[ a ; M col ∈ 𝕄 ] and M < |m and r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ] and (|c ap (|v ap (M))) ap (|v ap (|m)) = 0 and g ap (a) = |v ap (M) and [ ∀ i ∈ 𝕄 . (i {/}= a ⟹ g ap (i) = r ap (i)) ] ⟹ g ⇈ a suc and \< pr g ; a suc \> ⊑ \< pr |v ; M suc \> and [ ∀ i ∈ 𝕄 . (i < a suc ⟹ (|c ap (g ap (i))) ap (|v ap (|m)) = 0) ]` / ⇈. / ⊑. -| hyV / ⇈. , hym , L<S , L<K , L<s , L<T , L<irr , 𝕄0s v; YR <- `[ a ; M col ∈ 𝕄 ] and M < |m and r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ] and (|c ap (|v ap (M))) ap (|v ap (|m)) = 0 ⟹ [ ∃ g \, (g ⇈ a suc and \< pr g ; a suc \> ⊑ \< pr |v ; M suc \> and [ ∀ i ∈ 𝕄 . (i < a suc ⟹ (|c ap (g ap (i))) ap (|v ap (|m)) = 0) ]) ]` -| upd𝕄 , XR v; XB <- `[ a ; M col ∈ 𝕄 ] and M < |m and r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) {/}= 0) ] and (|c ap (|v ap (M))) ap (|v ap (|m)) {/}= 0 and g ap (a) = |v ap (M) and [ ∀ i ∈ 𝕄 . (i {/}= a ⟹ g ap (i) = r ap (i)) ] ⟹ g ⇈ a suc and \< pr g ; a suc \> ⊑ \< pr |v ; M suc \> and [ ∀ i ∈ 𝕄 . (i < a suc ⟹ (|c ap (g ap (i))) ap (|v ap (|m)) {/}= 0) ]` / ⇈. / ⊑. -| hyV / ⇈. , hym , L<S , L<K , L<s , L<T , L<irr , 𝕄0s v; YB <- `[ a ; M col ∈ 𝕄 ] and M < |m and r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) {/}= 0) ] and (|c ap (|v ap (M))) ap (|v ap (|m)) {/}= 0 ⟹ [ ∃ g \, (g ⇈ a suc and \< pr g ; a suc \> ⊑ \< pr |v ; M suc \> and [ ∀ i ∈ 𝕄 . (i < a suc ⟹ (|c ap (g ap (i))) ap (|v ap (|m)) {/}= 0) ]) ]` -| upd𝕄 , XB v; ESR <- `M ∈ 𝕄 and M < |m and [ ∃ a ∈ 𝕄 . [ ∃ b ∈ 𝕄 . a + b = M and [ ∃ r \, (r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ]) ] and [ ∃ u \, (u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ]) ] ] ] and (|c ap (|v ap (M))) ap (|v ap (|m)) = 0 ⟹ [ ∃ a ∈ 𝕄 . [ ∃ b ∈ 𝕄 . a + b = M suc and [ ∃ r \, (r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; M suc \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ]) ] and [ ∃ u \, (u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; M suc \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ]) ] ] ]` -| YR , KS , Lsuc+ , 𝕄0s v; ESB <- `M ∈ 𝕄 and M < |m and [ ∃ a ∈ 𝕄 . [ ∃ b ∈ 𝕄 . a + b = M and [ ∃ r \, (r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ]) ] and [ ∃ u \, (u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ]) ] ] ] and ¬ ((|c ap (|v ap (M))) ap (|v ap (|m)) = 0) ⟹ [ ∃ a ∈ 𝕄 . [ ∃ b ∈ 𝕄 . a + b = M suc and [ ∃ r \, (r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; M suc \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ]) ] and [ ∃ u \, (u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; M suc \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ]) ] ] ]` -| YB , KS , +𝕄 , 𝕄0s v; ES <- `M ∈ 𝕄 and M < |m and [ ∃ a ∈ 𝕄 . [ ∃ b ∈ 𝕄 . a + b = M and [ ∃ r \, (r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ]) ] and [ ∃ u \, (u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ]) ] ] ] ⟹ [ ∃ a ∈ 𝕄 . [ ∃ b ∈ 𝕄 . a + b = M suc and [ ∃ r \, (r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; M suc \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ]) ] and [ ∃ u \, (u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; M suc \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ]) ] ] ]` -| ESR , ESB v; Lsl <- `[ M ; N col ∈ 𝕄 ] and M suc ≤ N ⟹ M < N` / <. -| O p; EI <- `M ∈ 𝕄 and M ≤ |m ⟹ [ ∃ a ∈ 𝕄 . [ ∃ b ∈ 𝕄 . a + b = M and [ ∃ r \, (r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ]) ] and [ ∃ u \, (u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ]) ] ] ]` -| IND𝕄[C_:=`\{ cls M | M ≤ |m ⟹ [ ∃ a ∈ 𝕄 . [ ∃ b ∈ 𝕄 . a + b = M and [ ∃ r \, (r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ]) ] and [ ∃ u \, (u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; M \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ]) ] ] ] \}`] , E0 , ES , Lsl , L<≤ , hym , 𝕄0s v; EF <- `[ ∃ a ∈ 𝕄 . [ ∃ b ∈ 𝕄 . a + b = |M and [ ∃ r \, (r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; |M \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ]) ] and [ ∃ u \, (u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; |M \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ]) ] ] ]` -| EI , hyM v; ENUM -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , upd𝕄 h[fix]; section 付け足す txt 赤の隣の中の赤の完全部分に \(v(m)\) を付け足すと、\(v\) の中の1つ大きい赤の完全部分（APPR）。青も同じ（APPB）。 !let/thm APPR <- `[ K ; a ; m col ∈ 𝕄 ] and v ⇈ m suc and \< pr r ; a \> ⊑ \< pr v ; m \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (c ap (r ap (i))) ap (v ap (m)) = 0) ] and x ⇈ K and \< pr x ; K \> ⊑ \< pr r ; a \> and c ⊨₀ \< pr x ; K \> and g ap (K) = v ap (m) and [ ∀ i ∈ 𝕄 . (i {/}= K ⟹ g ap (i) = x ap (i)) ] ⟹ g ⇈ K suc and \< pr g ; K suc \> ⊑ \< pr v ; m suc \> and c ⊨₀ \< pr g ; K suc \>` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 prf hyN <- `[ |K ; |a ; |m col ∈ 𝕄 ]` ; hyV <- `|v ⇈ |m suc` ; hyR <- `\< pr |r ; |a \> ⊑ \< pr |v ; |m \>` ; hyT <- `[ ∀ i ∈ 𝕄 . (i < |a ⟹ (|c ap (|r ap (i))) ap (|v ap (|m)) = 0) ]` ; hyX <- `|x ⇈ |K` ; hyS <- `\< pr |x ; |K \> ⊑ \< pr |r ; |a \>` ; hyC <- `|c ⊨₀ \< pr |x ; |K \>` ; hyG <- `|g ap (|K) = |v ap (|m) and [ ∀ i ∈ 𝕄 . (i {/}= |K ⟹ |g ap (i) = |x ap (i)) ]` ; X1 <- `[ ∀ i ∈ 𝕄 . (i < |K ⟹ [ ∃ j ∈ 𝕄 . j < |m and |x ap (i) = |v ap (j) and (|c ap (|v ap (j))) ap (|v ap (|m)) = 0 ]) ]` -| hyS / ⊑. , hyR / ⊑. , hyT p; G1 <- `i ∈ 𝕄 and i < |K ⟹ |g ap (i) = |x ap (i)` -| hyG , L<irr p; W1 <- `j ∈ 𝕄 and j < |m ⟹ |v ap (j) < |v ap (|m)` -| hyV / ⇈. , L<K , L<s , hyN p; P1a <- `[ ∀ i ∈ 𝕄 . (i < |K suc ⟹ |g ap (i) ∈ 𝕄) ]` -| L<S , G1 , hyV / ⇈. , L<s , hyX / ⇈. , hyG , hyN v; P1b <- `[ i ; j col ∈ 𝕄 ] and i < j and j < |K ⟹ |g ap (i) < |g ap (j)` -| G1 , hyX / ⇈. , L<T , hyN p; P1c <- `i ∈ 𝕄 and i < |K ⟹ |g ap (i) < |g ap (|K)` -| G1 , X1 , W1 , hyG p; P1 <- `|g ⇈ |K suc` / ⇈. -| P1a , L<S , P1b , P1c , hyN v; P2 <- `\< pr |g ; |K suc \> ⊑ \< pr |v ; |m suc \>` / ⊑. -| L<S , G1 , X1 , L<K , L<s , hyG , hyN v; P3a <- `[ i ; j col ∈ 𝕄 ] and i < j and j < |K ⟹ (|c ap (|g ap (i))) ap (|g ap (j)) = 0` -| G1 , hyC / ⊨₀. , L<T , hyN p; P3b <- `i ∈ 𝕄 and i < |K ⟹ (|c ap (|g ap (i))) ap (|g ap (|K)) = 0` -| G1 , X1 , hyG p; P3 <- `|c ⊨₀ \< pr |g ; |K suc \>` / ⊨₀. -| L<S , P3a , P3b , hyN v; PF <- `|g ⇈ |K suc and \< pr |g ; |K suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₀ \< pr |g ; |K suc \>` -| P1 , P2 , P3 p; APPR -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 h[fix]; !let/thm APPB <- `[ K ; a ; m col ∈ 𝕄 ] and v ⇈ m suc and \< pr r ; a \> ⊑ \< pr v ; m \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (c ap (r ap (i))) ap (v ap (m)) {/}= 0) ] and x ⇈ K and \< pr x ; K \> ⊑ \< pr r ; a \> and c ⊨₁ \< pr x ; K \> and g ap (K) = v ap (m) and [ ∀ i ∈ 𝕄 . (i {/}= K ⟹ g ap (i) = x ap (i)) ] ⟹ g ⇈ K suc and \< pr g ; K suc \> ⊑ \< pr v ; m suc \> and c ⊨₁ \< pr g ; K suc \>` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 prf hyN <- `[ |K ; |a ; |m col ∈ 𝕄 ]` ; hyV <- `|v ⇈ |m suc` ; hyR <- `\< pr |r ; |a \> ⊑ \< pr |v ; |m \>` ; hyT <- `[ ∀ i ∈ 𝕄 . (i < |a ⟹ (|c ap (|r ap (i))) ap (|v ap (|m)) {/}= 0) ]` ; hyX <- `|x ⇈ |K` ; hyS <- `\< pr |x ; |K \> ⊑ \< pr |r ; |a \>` ; hyC <- `|c ⊨₁ \< pr |x ; |K \>` ; hyG <- `|g ap (|K) = |v ap (|m) and [ ∀ i ∈ 𝕄 . (i {/}= |K ⟹ |g ap (i) = |x ap (i)) ]` ; X1 <- `[ ∀ i ∈ 𝕄 . (i < |K ⟹ [ ∃ j ∈ 𝕄 . j < |m and |x ap (i) = |v ap (j) and (|c ap (|v ap (j))) ap (|v ap (|m)) {/}= 0 ]) ]` -| hyS / ⊑. , hyR / ⊑. , hyT p; G1 <- `i ∈ 𝕄 and i < |K ⟹ |g ap (i) = |x ap (i)` -| hyG , L<irr p; W1 <- `j ∈ 𝕄 and j < |m ⟹ |v ap (j) < |v ap (|m)` -| hyV / ⇈. , L<K , L<s , hyN p; P1a <- `[ ∀ i ∈ 𝕄 . (i < |K suc ⟹ |g ap (i) ∈ 𝕄) ]` -| L<S , G1 , hyV / ⇈. , L<s , hyX / ⇈. , hyG , hyN v; P1b <- `[ i ; j col ∈ 𝕄 ] and i < j and j < |K ⟹ |g ap (i) < |g ap (j)` -| G1 , hyX / ⇈. , L<T , hyN p; P1c <- `i ∈ 𝕄 and i < |K ⟹ |g ap (i) < |g ap (|K)` -| G1 , X1 , W1 , hyG p; P1 <- `|g ⇈ |K suc` / ⇈. -| P1a , L<S , P1b , P1c , hyN v; P2 <- `\< pr |g ; |K suc \> ⊑ \< pr |v ; |m suc \>` / ⊑. -| L<S , G1 , X1 , L<K , L<s , hyG , hyN v; P3a <- `[ i ; j col ∈ 𝕄 ] and i < j and j < |K ⟹ (|c ap (|g ap (i))) ap (|g ap (j)) {/}= 0` -| G1 , hyC / ⊨₁. , L<T , hyN p; P3b <- `i ∈ 𝕄 and i < |K ⟹ (|c ap (|g ap (i))) ap (|g ap (|K)) {/}= 0` -| G1 , X1 , hyG p; P3 <- `|c ⊨₁ \< pr |g ; |K suc \>` / ⊨₁. -| L<S , P3a , P3b , hyN v; PF <- `|g ⇈ |K suc and \< pr |g ; |K suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₁ \< pr |g ; |K suc \>` -| P1 , P2 , P3 p; APPB -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 h[fix]; section 帰納法の1段 txt 赤の隣が \(n\) 個以上なら、そこに \((P, Q+1)\) の場合を当て、赤の完全部分なら \(v(m)\) を付け足します。青の隣が \(k\) 個以上なら同様です。\(n + k \le m\) なのでどちらかが起きます（Lsplit）。 let/thm STEP <- `[ P ; Q ; n ; k ; m col ∈ 𝕄 ] and [ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and n ≤ L ⟹ [ ∃ x \, ((x ⇈ P and \< pr x ; P \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; P \>) or (x ⇈ Q suc and \< pr x ; Q suc \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; Q suc \>)) ]) ] ] ] and [ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and k ≤ L ⟹ [ ∃ x \, ((x ⇈ P suc and \< pr x ; P suc \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; P suc \>) or (x ⇈ Q and \< pr x ; Q \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; Q \>)) ]) ] ] ] and v ⇈ m suc and (n + k) suc ≤ m suc ⟹ [ ∃ x \, ((x ⇈ P suc and \< pr x ; P suc \> ⊑ \< pr v ; m suc \> and c ⊨₀ \< pr x ; P suc \>) or (x ⇈ Q suc and \< pr x ; Q suc \> ⊑ \< pr v ; m suc \> and c ⊨₁ \< pr x ; Q suc \>)) ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , upd𝕄 , 1. prf hyN <- `[ |P ; |Q ; |n ; |k ; |m col ∈ 𝕄 ]` ; hyR1 <- `[ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and |n ≤ L ⟹ [ ∃ x \, ((x ⇈ |P and \< pr x ; |P \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; |P \>) or (x ⇈ |Q suc and \< pr x ; |Q suc \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; |Q suc \>)) ]) ] ] ]` ; hyR2 <- `[ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and |k ≤ L ⟹ [ ∃ x \, ((x ⇈ |P suc and \< pr x ; |P suc \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; |P suc \>) or (x ⇈ |Q and \< pr x ; |Q \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; |Q \>)) ]) ] ] ]` ; hyV <- `|v ⇈ |m suc` ; hyL <- `(|n + |k) suc ≤ |m suc` ; SS <- `[ x ; y col ∈ 𝕄 ] and x suc ≤ y suc ⟹ x ≤ y` / ≤. -| +𝕄 , suc𝕄 , +∈𝕄 p; Lnk <- `|n + |k ≤ |m` -| SS , hyL , hyN , +∈𝕄 p; EM <- `[ ∃ a ∈ 𝕄 . [ ∃ b ∈ 𝕄 . a + b = |m and [ ∃ r \, (r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; |m \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ]) ] and [ ∃ u \, (u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; |m \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ]) ] ] ]` -| ENUM , hyN , hyV , L≤R v; ST <- `\< pr x ; K \> ⊑ \< pr r ; a \> and \< pr r ; a \> ⊑ \< pr |v ; |m \> ⟹ \< pr x ; K \> ⊑ \< pr |v ; |m suc \>` / ⊑. -| L<K , hyN p; HR <- `a ∈ 𝕄 and r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; |m \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ] and |n ≤ a ⟹ [ ∃ x \, ((x ⇈ |P and \< pr x ; |P \> ⊑ \< pr r ; a \> and |c ⊨₀ \< pr x ; |P \>) or (x ⇈ |Q suc and \< pr x ; |Q suc \> ⊑ \< pr r ; a \> and |c ⊨₁ \< pr x ; |Q suc \>)) ]` -| hyR1 v; GR <- `a ∈ 𝕄 and r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; |m \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ] and x ⇈ |P and \< pr x ; |P \> ⊑ \< pr r ; a \> and |c ⊨₀ \< pr x ; |P \> and g ap (|P) = |v ap (|m) and [ ∀ i ∈ 𝕄 . (i {/}= |P ⟹ g ap (i) = x ap (i)) ] ⟹ [ ∃ x \, ((x ⇈ |P suc and \< pr x ; |P suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₀ \< pr x ; |P suc \>) or (x ⇈ |Q suc and \< pr x ; |Q suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₁ \< pr x ; |Q suc \>)) ]` -| APPR , hyN , hyV v; AR <- `a ∈ 𝕄 and r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; |m \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ] and x ⇈ |P and \< pr x ; |P \> ⊑ \< pr r ; a \> and |c ⊨₀ \< pr x ; |P \> ⟹ [ ∃ x \, ((x ⇈ |P suc and \< pr x ; |P suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₀ \< pr x ; |P suc \>) or (x ⇈ |Q suc and \< pr x ; |Q suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₁ \< pr x ; |Q suc \>)) ]` -| upd𝕄 , GR v; OR <- `a ∈ 𝕄 and r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; |m \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ] and x ⇈ |Q suc and \< pr x ; |Q suc \> ⊑ \< pr r ; a \> and |c ⊨₁ \< pr x ; |Q suc \> ⟹ [ ∃ x \, ((x ⇈ |P suc and \< pr x ; |P suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₀ \< pr x ; |P suc \>) or (x ⇈ |Q suc and \< pr x ; |Q suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₁ \< pr x ; |Q suc \>)) ]` -| ST , hyN v; CR <- `a ∈ 𝕄 and r ⇈ a and \< pr r ; a \> ⊑ \< pr |v ; |m \> and [ ∀ i ∈ 𝕄 . (i < a ⟹ (|c ap (r ap (i))) ap (|v ap (|m)) = 0) ] and |n ≤ a ⟹ [ ∃ x \, ((x ⇈ |P suc and \< pr x ; |P suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₀ \< pr x ; |P suc \>) or (x ⇈ |Q suc and \< pr x ; |Q suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₁ \< pr x ; |Q suc \>)) ]` -| HR , AR , OR v; HB <- `b ∈ 𝕄 and u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; |m \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ] and |k ≤ b ⟹ [ ∃ x \, ((x ⇈ |P suc and \< pr x ; |P suc \> ⊑ \< pr u ; b \> and |c ⊨₀ \< pr x ; |P suc \>) or (x ⇈ |Q and \< pr x ; |Q \> ⊑ \< pr u ; b \> and |c ⊨₁ \< pr x ; |Q \>)) ]` -| hyR2 v; GB <- `b ∈ 𝕄 and u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; |m \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ] and x ⇈ |Q and \< pr x ; |Q \> ⊑ \< pr u ; b \> and |c ⊨₁ \< pr x ; |Q \> and g ap (|Q) = |v ap (|m) and [ ∀ i ∈ 𝕄 . (i {/}= |Q ⟹ g ap (i) = x ap (i)) ] ⟹ [ ∃ x \, ((x ⇈ |P suc and \< pr x ; |P suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₀ \< pr x ; |P suc \>) or (x ⇈ |Q suc and \< pr x ; |Q suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₁ \< pr x ; |Q suc \>)) ]` -| APPB , hyN , hyV v; AB <- `b ∈ 𝕄 and u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; |m \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ] and x ⇈ |Q and \< pr x ; |Q \> ⊑ \< pr u ; b \> and |c ⊨₁ \< pr x ; |Q \> ⟹ [ ∃ x \, ((x ⇈ |P suc and \< pr x ; |P suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₀ \< pr x ; |P suc \>) or (x ⇈ |Q suc and \< pr x ; |Q suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₁ \< pr x ; |Q suc \>)) ]` -| upd𝕄 , GB v; OB <- `b ∈ 𝕄 and u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; |m \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ] and x ⇈ |P suc and \< pr x ; |P suc \> ⊑ \< pr u ; b \> and |c ⊨₀ \< pr x ; |P suc \> ⟹ [ ∃ x \, ((x ⇈ |P suc and \< pr x ; |P suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₀ \< pr x ; |P suc \>) or (x ⇈ |Q suc and \< pr x ; |Q suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₁ \< pr x ; |Q suc \>)) ]` -| ST , hyN v; CB <- `b ∈ 𝕄 and u ⇈ b and \< pr u ; b \> ⊑ \< pr |v ; |m \> and [ ∀ i ∈ 𝕄 . (i < b ⟹ (|c ap (u ap (i))) ap (|v ap (|m)) {/}= 0) ] and |k ≤ b ⟹ [ ∃ x \, ((x ⇈ |P suc and \< pr x ; |P suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₀ \< pr x ; |P suc \>) or (x ⇈ |Q suc and \< pr x ; |Q suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₁ \< pr x ; |Q suc \>)) ]` -| HB , AB , OB v; HF <- `[ ∃ x \, ((x ⇈ |P suc and \< pr x ; |P suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₀ \< pr x ; |P suc \>) or (x ⇈ |Q suc and \< pr x ; |Q suc \> ⊑ \< pr |v ; |m suc \> and |c ⊨₁ \< pr x ; |Q suc \>)) ]` -| EM , Lsplit , Lnk , CR , CB , hyN v; STEP -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , upd𝕄 , 1. h[fix]; section Ramsey の定理 txt どの \(P, Q\) にも、長さ \(N\) 以上のどの増加列 \(v\) とどの色付け \(c\) についても、\(v\) の中に大きさ \(P\) の赤の完全部分か大きさ \(Q\) の青の完全部分がある、という \(N\) があります。\(P\) と \(Q\) についての二重の帰納法で、\(N\) は \((n + k) + 1\) と取ります（STEP）。 let/thm Ramsey <- `[ P ; Q col ∈ 𝕄 ] ⟹ [ ∃ N ∈ 𝕄 . [ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and N ≤ L ⟹ [ ∃ x \, ((x ⇈ P and \< pr x ; P \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; P \>) or (x ⇈ Q and \< pr x ; Q \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; Q \>)) ]) ] ] ] ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , upd𝕄 , 1. prf Lm <- `[ x ; L col ∈ 𝕄 ] and x suc ≤ L ⟹ [ ∃ m ∈ 𝕄 . L = m suc ]` / ≤. -| +𝕄 , +∈𝕄 p; LU <- `[ P ; Q ; n ; k col ∈ 𝕄 ] and [ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and n ≤ L ⟹ [ ∃ x \, ((x ⇈ P and \< pr x ; P \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; P \>) or (x ⇈ Q suc and \< pr x ; Q suc \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; Q suc \>)) ]) ] ] ] and [ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and k ≤ L ⟹ [ ∃ x \, ((x ⇈ P suc and \< pr x ; P suc \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; P suc \>) or (x ⇈ Q and \< pr x ; Q \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; Q \>)) ]) ] ] ] ⟹ [ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and (n + k) suc ≤ L ⟹ [ ∃ x \, ((x ⇈ P suc and \< pr x ; P suc \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; P suc \>) or (x ⇈ Q suc and \< pr x ; Q suc \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; Q suc \>)) ]) ] ] ]` -| STEP , Lm , +∈𝕄 , 𝕄0s v; LQ <- `P ∈ 𝕄 and [ ∀ Q ∈ 𝕄 . [ ∃ N ∈ 𝕄 . [ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and N ≤ L ⟹ [ ∃ x \, ((x ⇈ P and \< pr x ; P \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; P \>) or (x ⇈ Q and \< pr x ; Q \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; Q \>)) ]) ] ] ] ] ] ⟹ [ ∀ Q ∈ 𝕄 . [ ∃ N ∈ 𝕄 . [ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and N ≤ L ⟹ [ ∃ x \, ((x ⇈ P suc and \< pr x ; P suc \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; P suc \>) or (x ⇈ Q and \< pr x ; Q \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; Q \>)) ]) ] ] ] ] ]` -| IND𝕄[C_:=`\{ cls Q | [ ∃ N ∈ 𝕄 . [ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and N ≤ L ⟹ [ ∃ x \, ((x ⇈ P suc and \< pr x ; P suc \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; P suc \>) or (x ⇈ Q and \< pr x ; Q \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; Q \>)) ]) ] ] ] ] \}`] , RP0 , LU , +∈𝕄 , 𝕄0s v; RA <- `[ ∀ P ∈ 𝕄 . [ ∀ Q ∈ 𝕄 . [ ∃ N ∈ 𝕄 . [ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and N ≤ L ⟹ [ ∃ x \, ((x ⇈ P and \< pr x ; P \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; P \>) or (x ⇈ Q and \< pr x ; Q \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; Q \>)) ]) ] ] ] ] ] ]` -| IND𝕄[C_:=`\{ cls P | [ ∀ Q ∈ 𝕄 . [ ∃ N ∈ 𝕄 . [ ∀ c \, [ ∀ v \, [ ∀ L ∈ 𝕄 . (v ⇈ L and N ≤ L ⟹ [ ∃ x \, ((x ⇈ P and \< pr x ; P \> ⊑ \< pr v ; L \> and c ⊨₀ \< pr x ; P \>) or (x ⇈ Q and \< pr x ; Q \> ⊑ \< pr v ; L \> and c ⊨₁ \< pr x ; Q \>)) ]) ] ] ] ] ] \}`] , R0Q , LQ , 𝕄0s v; Ramsey -| RA v; Ramsey -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , upd𝕄 , 1. h;
表示（保存しません）
保存にはMatheliaへのログインが要ります。