未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
freek100/52.book
ヘッダ
行番号
title 部分集合の個数 formel /common/default thmel /common/zf option review quick:true;
section 一階述語論理 subsection 通常の論理記号 word ⊤ ⊥ word ¬ word and or ⇒ ⇔ word ∀ ∃ word = word =_ subsection 高度な論理記号 word and_ ⟹ ⟺ lower and_ lower ⟹ lower ⟺ word {/} lower {/} subsection andを含む略記法 abbr And abbr col abbr chain subsection 量化子の略記法 abbr ∀ abbr ∃ abbr ∀+ abbr ∃+ abbr ∀* abbr ∃* abbr ∀*+ abbr ∃*+ newpage section 基本記号① subsection 2項述語の性質 word :R :T :X lower :R lower :T lower :X subsection 所属関係と内包記法 word ∈_ word ∈ word \cls abbr cls abbr cls+ subsection 外延性 prop =_. prop =. subsection 包含関係 word ⊂_ ⊊_ prop ⊂_. prop ⊊_. word ⊂ ⊊ prop ⊂. prop ⊊. prop/thm ⊊.. ◀ W. prf ⊊.. // W. -| O p; ⊊.. -| W. h; newpage section 集合・クラスの最初の例 subsection 宇宙、空集合 word 𝕍 prop 𝕍. word ∅ prop ∅. !prop/thm ∅.' ◀ W. prf ∅.' // W. -| O p; ∅.' -| W. h; subsection 有限集合 word set\n abbr set prop set\n. !prop/thm set\n.' ◀ W. at \n=1..4 prf set\n.' /1 =. / set\n. -| O p; set\n.' -| W. h; subsection 合併、共通部分、差 word ∪_ ∩_ ∖_ prop ∪_. prop ∩_. prop ∖_. word xs prop xs. word ∪ ∩ prop ∪. prop ∩. prop ∖. subsection 総合併、総共通部分 word ⋃_ ⋂_ prop ⋃_. prop ⋂_. word ⋃ ⋂ prop ⋃. prop ⋂. !prop/thm ⋂.' ◀ W. prf ⋂.' -| ⋂. / ∅.' p; ⋂.' -| W. h; newpage section 基本記号② subsection 一意量化子 abbr ！ abbr ∃！ abbr ！+ abbr ∃！+ subsection 集合となるクラス word Exi prop Exi. word 𝕍0 prop 𝕍0. prop ax_r <- `∀ x \, [ ！ y \, x ??p^ y ] ⟹ ∀ X \, Exi \{ cls y | [ ∃ x ∈ X . x ??p^ y ] \}` prop/thm ax_s ◀ ax_r prf ax_s --| ax_r[??p^:=`x ∈_ C_ and y = x`] v; ax_s ◀ ax_r h; subsection 内包記法の拡張 abbr Cls abbr Cls+ abbr -Cls subsection 関数の像 word {^} lower {^} word {^*} {*^} {^^} lower {^*} lower {*^} lower {^^} newpage section 代数の最初の例 subsection アロー関数 word \fn abbr fn subsection べき集合 word ℘ prop ℘. !prop/thm ℘.' ◀ W. prf ℘.' -| W. p; section 順序対 subsection 順序対 word \pr abbr pr word ◁ ▷ prop ◁. prop ▷. prop/thm pr:0 ◀ W. prf pr:0 -| ◁. ,, ▷. p; pr:0 -| W. h; word ^◁ ^▷ prop ^◁. prop ^▷. subsection 直積、関係 word ^^pr_ prop ^^pr_. word ^^pr prop ^^pr. word Rel prop Rel. prop/thm Rel.' ◀ W. prf Rel.' /// W.!=. -| O p; Rel.' -| W. h; subsection 代入 word ^◁! prop ^◁!. word* ap prop ap. word* *^ap prop *^ap. subsection 対の入れ替え、逆関係 word sw prop sw. word ^sw prop ^sw. subsection 関係の合成 word ∘ prop ∘. newpage section 写像 subsection 写像の集合 word →_ prop →_. !prop/thm →_.' ◀ W. prf →_.' // W.!=. -| O {Y_.-} p; →_.' -| W. h; word → prop →. !prop/thm →.' ◀ W. prf →.' / →. -| O {→_.'} p; →.' -| W. h; prop/thm →.. ◀ W. prf →.. // W.'!=. -| pr:0 p; →.. -| W. h; !prop/thm →..' ◀ W. prf →..' / →.. / ⊂. / ^▷. -| pr:0 ,, ap. p; →..' -| W. h; prop/thm →∘ ◀ W. prf →∘ / →.' / ∘. -| pr:0 p; →∘ -| W. h; subsection 制限 word rest prop rest. word Rest prop Rest. newpage section 集合の大きさ比較 subsection 単射、全射、全単射 word →I →S →IS prop →I. !prop/thm →I.' ◀ W. prf →I.' //// W.!=. -| sw. p; →I.' -| W. h; prop →S. !prop/thm →S.' ◀ W. prf →S.' / →S. / →.. -| ^▷. ,, =. ,, ⊂. p; →S.' -| W. h; prop/thm →S:0 ◀ W. prf →S:0 / →S. -| O p; →S:0 -| W. h; prop →IS. !prop/thm →IS.' ◀ W. prf →IS.' /// W.'!=. -| pr:0 p; →IS.' -| W. h; prop/thm →IS^sw ◀ W. prf →IS^sw /// W.'!=. -| sw. p; →IS^sw -| W. h; prop/thm →I∘ ◀ W. prf →I∘ / →I.' / ∘. -| →∘ ,, pr:0 p; →I∘ -| W. h; prop/thm →S∘ ◀ W. prf →S∘ / →S.' / ∘. -| →∘ ,, pr:0 ,, →.' p; →S∘ -| W. h; prop/thm →IS∘ ◀ W. prf →IS∘ / →IS. / ∩. -| →I∘ ,, →S∘ p; →IS∘ -| W. h; subsection 恒等写像 word id prop id. prop/thm id:0 ◀ W. prf id:0 /// W.'!=. -| pr:0 p; id:0 -| W. h; subsection 濃度 word =# ≤# <# prop =#. prop ≤#. prop <#. !prop/thm =#.' ◀ W. prf =#.' / =#. / ∅.' -| O p; =#.' -| W. h; !prop/thm ≤#.' ◀ W. prf ≤#.' / ≤#. / ∅.' -| O p; ≤#.' -| W. h; prop/thm =#:RTX ◀ W. prf =#:RTX / =#.' -| id:0 ,, →IS∘ ,, →IS^sw p; =#:RTX -| W. h; !prop/thm =#:X ◀ W. prf =#:X / =#.' -| →IS^sw p; =#:X -| W. h; prop/thm ≤#:RT ◀ W. prf ≤#:RT / ≤#.' -| id:0 / →IS. / ∩. ,, →I∘ p; ≤#:RT -| W. h; prop/thm sub_≤# ◀ W. prf L <- `X ⊂ Y ⟹ id _ X ∈ X →I Y` /// W.'!=. -| pr:0 p; sub_≤# / ≤#.' -| L p; sub_≤# -| W. h; prop/thm =#0 ◀ W. prf =#0 //// W.'!=. -| O p; =#0 -| W. h; subsection 選択公理 word choice prop choice. !prop/thm choice.' ◀ W. prf choice.' // W.'!=. -| pr:0 ,, ap. ,, ^◁!. p; choice.' -| W. h; prop ax_c subsection 直積 word ∏ prop ∏. !prop/thm ∏.' ◀ W. prf ∏.' -| ∏. v; ∏.' -| W. h; prop Dp_c section 自然数 subsection 0と後続関数 word 0 prop 0. !prop/thm 0.' ◀ W. prf 0.' / W. -| O p; 0.' -| W. h; word suc ^suc prop suc. !prop/thm suc.' ◀ W. prf suc.' // W.!=. -| O p; suc.' -| W. h; prop ^suc. subsection 帰納法 word Ind prop Ind. !prop/thm Ind.' ◀ W. prf Ind.' // W.'!=. -| O p; Ind.' -| W. h; word 𝕄 prop 𝕄. !prop/thm 𝕄1 ◀ W. prf 𝕄1 /// W.'!=. -| O p; 𝕄1 -| W. h; !prop/thm <𝕄:l ◀ W. ,, ax_s prf A_ := `\{ cls n ∈ 𝕄 | [ ∀ m ∈ n . m ⊊ n ] \}` ; L0 <- `0 ∈ 𝕄` / 𝕄. -| O p; LAs <- `A_ ⊂_ 𝕄` /// W. -| O p; LEA <- `Exi A_` -| LAs ,, ax_s[C_:=`A_`] p; LE <- `[ ∃ A \, [ ∀ n (n ∈ A ⟺ n ∈ 𝕄 and [ ∀ m ∈ n . m ⊊ n ]) ] ]` -| LEA p; LI <- `[ ∀ n (n ∈ A ⟺ n ∈ 𝕄 and [ ∀ m ∈ n . m ⊊ n ]) ] ⟹ A ∈_ Ind` / ⊊.. / ⊂. / ^suc. -| L0 ,, 𝕄1 ,, suc.' ,, 0.' v; LM <- `[ ∀ n (n ∈ A ⟺ n ∈ 𝕄 and [ ∀ m ∈ n . m ⊊ n ]) ] ⟹ 𝕄 ⊂ A` -| LI ,, 𝕄. ,, ⊂. p; <𝕄:l -| LE ,, LM ,, ⊂. p; <𝕄:l -| W. ,, ax_s h; !prop/thm <𝕄:r ◀ W. ,, ax_s prf A_ := `\{ cls n ∈ 𝕄 | [ ∀ m ∈ 𝕄 . (m ⊊ n ⇒ m ∈ n) ] \}` ; L0 <- `0 ∈ 𝕄` / 𝕄. -| O p; LAs <- `A_ ⊂_ 𝕄` /// W. -| O p; LEA <- `Exi A_` -| LAs ,, ax_s[C_:=`A_`] p; LE <- `[ ∃ A \, [ ∀ n (n ∈ A ⟺ n ∈ 𝕄 and [ ∀ m ∈ 𝕄 . (m ⊊ n ⇒ m ∈ n) ]) ] ]` -| LEA p; Le1 <- `[ m ; n col ∈ 𝕄 ] and m ⊊ n suc ⟹ m ⊊ n or m = n` / ⊊.. / =. / ⊂. / suc.' -| 𝕄1 ,, <𝕄:l / ⊊.. / ⊂. p; LI <- `[ ∀ n (n ∈ A ⟺ n ∈ 𝕄 and [ ∀ m ∈ 𝕄 . (m ⊊ n ⇒ m ∈ n) ]) ] ⟹ A ∈_ Ind` / ⊊.. / ⊂. / ^suc. -| L0 ,, 𝕄1 ,, suc.' ,, 0.' ,, Le1 / ⊊.. / ⊂. ,, =. v; LM <- `[ ∀ n (n ∈ A ⟺ n ∈ 𝕄 and [ ∀ m ∈ 𝕄 . (m ⊊ n ⇒ m ∈ n) ]) ] ⟹ 𝕄 ⊂ A` -| LI ,, 𝕄. ,, ⊂. v; <𝕄:r -| LE ,, LM ,, ⊂. p; <𝕄:r -| W. ,, ax_s h; prop/thm <𝕄:T ◀ W. ,, ax_s prf A_ := `\{ cls n ∈ 𝕄 | [ ∀ m ∈ 𝕄 . m ⊂ n or n ⊂ m ] \}` ; L0 <- `0 ∈ 𝕄` / 𝕄. -| O p; LAs <- `A_ ⊂_ 𝕄` /// W. -| O p; LEA <- `Exi A_` -| LAs ,, ax_s[C_:=`A_`] p; LE <- `[ ∃ A \, [ ∀ n (n ∈ A ⟺ n ∈ 𝕄 and [ ∀ m ∈ 𝕄 . m ⊂ n or n ⊂ m ]) ] ]` -| LEA p; LI <- `[ ∀ n (n ∈ A ⟺ n ∈ 𝕄 and [ ∀ m ∈ 𝕄 . m ⊂ n or n ⊂ m ]) ] ⟹ A ∈_ Ind` / ⊂. / ^suc. -| L0 ,, 𝕄1 ,, suc.' ,, 0.' ,, <𝕄:r / ⊊.. / ⊂. v; LM <- `[ ∀ n (n ∈ A ⟺ n ∈ 𝕄 and [ ∀ m ∈ 𝕄 . m ⊂ n or n ⊂ m ]) ] ⟹ 𝕄 ⊂ A` -| LI ,, 𝕄. ,, ⊂. v; <𝕄:T -| LE ,, LM ,, ⊂. p; <𝕄:T -| W. ,, ax_s h; subsection 自然数の記号 word \n prop \n. !prop/thm \n.' ◀ W. at \n=1..5 prf \n.' /// W. -| O p; \n.' -| W. h; prop/thm \n.. ◀ W. at \n=1..5 prf \n.. / W. /// W.!=. -| O p; \n.. -| W. h; !prop/thm ≠1 ◀ O prf ≠1 -| O p; prop/thm ≠\n ◀ W. at \n=2..5 prf ≠\n // W. -| ≠\n-1 p; ≠\n -| W. h; newpage section 列 subsection 列 word ary\n abbr ary prop ary\n. !prop/thm ary1R ◀ W. prf ary1R /// W.!=.!0. -| pr:0 p; ary1R -| W. h; !prop/thm ary\nR ◀ W. at \n=2..4 prf ary\nR /// W.!=.!0. -| ≠\n ,, pr:0 p; ary\nR -| W. h; !prop/thm ary1> ◀ W. prf ary1> / W. // W.!=. -| pr:0 p; ary1> -| W. h; !prop/thm ary\n> ◀ W. at \n=2..4 prf ary\n> / W. // W.!=. -| pr:0 p; ary\n> -| W. h; prop/thm ary\nS ◀ W. at \n=1..4 prf ary\nS -| ary\nR ,, ary\n> ,, →S:0 p; ary\nS -| W. h; prop/thm ary1IS ◀ W. prf LI <- `\< ary x \> ∈ 1 →I \{ set x \}` / →I.' /// W.!=.!0. -| ary1S / →S.' /// W.!=.!0. ,, pr:0 p; ary1IS / →IS. / ∩. -| LI ,, ary1S p; ary1IS -| W. h; subsection 自然数と濃度 prop/thm =#1 ◀ W. prf =#1 / =#:X / =#.' [⇒ //// W.'!=. -| pr:0 || <= -| ary1IS] p; =#1 -| W. h; newpage section 有限と無限 subsection 鳩の巣原理 !let/thm Lfun <- `f ∈ X →I Y ⟹ f ∈ X → Y` ◀ W. prf Lfun / →I.' -| O p; Lfun -| W. h; !let/thm Lsw1 <- `f ∈ X → Y ⟹ ( \< pr y ; x \> ∈ f ^sw ⟺ \< pr x ; y \> ∈ f )` ◀ W. prf Lsw1 / ^sw. -| sw. ,, →.' p; Lsw1 -| W. h; !let/thm Lfval <- `f ∈ X → Y and \< pr x ; y \> ∈ f ⟹ y ∈ Y` ◀ W. prf Lfval / →.' -| pr:0 p; Lfval -| W. h; !let/thm Lftot <- `f ∈ X → Y and x ∈ X ⟹ [ ∃ y \, \< pr x ; y \> ∈ f ]` ◀ W. prf Lftot / →.' -| O p; Lftot -| W. h; !let/thm Lfuniq <- `f ∈ X → Y and x ∈ X and \< pr x ; y0 \> ∈ f and \< pr x ; y1 \> ∈ f ⟹ y0 = y1` ◀ W. prf Lfuniq / →.' -| O p; Lfuniq -| W. h; !let/thm Lfinj <- `f ∈ X →I Y and \< pr x0 ; y \> ∈ f and \< pr x1 ; y \> ∈ f ⟹ x0 = x1` ◀ W. prf Lfinj / →I.' -| O p; Lfinj -| W. h; !let/thm LuD <- `x ∈ X ∪ \{ set c \} ⟺ x ∈ X or x = c` ◀ W. prf LuD // W.'!=. -| O p; LuD -| W. h; !let/thm Lfdom <- `f ∈ X → Y and \< pr x ; y \> ∈ f ⟹ x ∈ X` ◀ W. prf Lfdom / →.' -| pr:0 p; Lfdom -| W. h; !let/thm Lpair <- `f ∈ X → Y and p ∈ f ⟹ [ ∃ x ; y \, p = \< pr x ; y \> ]` ◀ W. prf Lpair / →.' -| O p; Lpair -| W. h; !let/thm Lsw <- `a {/}∈ A and b {/}∈ B and (A ∪ \{ set a \}) ≤# (B ∪ \{ set b \}) ⟹ A ≤# B` ◀ W. prf G_ := `(f ∩ (A ^^pr B)) ∪ ((((f ^sw) *^ap (\{ set b \})) ∩ A) ^^pr (f *^ap (\{ set a \})))` ; LGmem <- `f ∈ X → Y ⟹ [ ∀ u ; v (\< pr u ; v \> ∈ G_ ⇔ ((\< pr u ; v \> ∈ f and u ∈ A and v ∈ B) or (u ∈ A and \< pr u ; b \> ∈ f and \< pr a ; v \> ∈ f))) ]` / ∪. / ∩. / ^^pr. / ∩. / *^ap. -| Lsw1 ,, pr:0 ,, set1. p; LGpair <- `p ∈ G_ ⟹ [ ∃ u ; v \, p = \< pr u ; v \> ]` / ∪. / ∩. / ^^pr. -| O p; LGm <- `f ∈ (A ∪ \{ set a \}) →I (B ∪ \{ set b \}) and G = G_ ⟹ [ ∀ u ; v (\< pr u ; v \> ∈ G ⇔ ((\< pr u ; v \> ∈ f and u ∈ A and v ∈ B) or (u ∈ A and \< pr u ; b \> ∈ f and \< pr a ; v \> ∈ f))) ]` -| LGmem ,, Lfun p; LGp <- `G = G_ ⟹ [ ∀ p ∈ G . [ ∃ u ; v \, p = \< pr u ; v \> ] ]` -| LGpair p; LGv2 <- `a {/}∈ A and f ∈ (A ∪ \{ set a \}) →I (B ∪ \{ set b \}) and u ∈ A and \< pr u ; b \> ∈ f and \< pr a ; v \> ∈ f ⟹ v ∈ B` -| Lfval ,, Lfinj ,, Lfun ,, LuD p; LGval <- `a {/}∈ A and f ∈ (A ∪ \{ set a \}) →I (B ∪ \{ set b \}) and [ ∀ u ; v (\< pr u ; v \> ∈ G ⇔ ((\< pr u ; v \> ∈ f and u ∈ A and v ∈ B) or (u ∈ A and \< pr u ; b \> ∈ f and \< pr a ; v \> ∈ f))) ] and \< pr u ; v \> ∈ G ⟹ u ∈ A and v ∈ B` -| LGv2 p; LGtot <- `f ∈ (A ∪ \{ set a \}) →I (B ∪ \{ set b \}) and [ ∀ u ; v (\< pr u ; v \> ∈ G ⇔ ((\< pr u ; v \> ∈ f and u ∈ A and v ∈ B) or (u ∈ A and \< pr u ; b \> ∈ f and \< pr a ; v \> ∈ f))) ] and x ∈ A ⟹ [ ∃ y \, \< pr x ; y \> ∈ G ]` -| Lftot ,, Lfval ,, Lfun ,, LuD p; LGuniq <- `b {/}∈ B and f ∈ (A ∪ \{ set a \}) →I (B ∪ \{ set b \}) and [ ∀ u ; v (\< pr u ; v \> ∈ G ⇔ ((\< pr u ; v \> ∈ f and u ∈ A and v ∈ B) or (u ∈ A and \< pr u ; b \> ∈ f and \< pr a ; v \> ∈ f))) ] and x ∈ A and \< pr x ; y0 \> ∈ G and \< pr x ; y1 \> ∈ G ⟹ y0 = y1` -| Lfuniq ,, Lfun ,, LuD p; LGinj <- `a {/}∈ A and f ∈ (A ∪ \{ set a \}) →I (B ∪ \{ set b \}) and [ ∀ u ; v (\< pr u ; v \> ∈ G ⇔ ((\< pr u ; v \> ∈ f and u ∈ A and v ∈ B) or (u ∈ A and \< pr u ; b \> ∈ f and \< pr a ; v \> ∈ f))) ] and \< pr x0 ; y \> ∈ G and \< pr x1 ; y \> ∈ G ⟹ x0 = x1` -| Lfinj p; LGmap <- `a {/}∈ A and b {/}∈ B and f ∈ (A ∪ \{ set a \}) →I (B ∪ \{ set b \}) and [ ∀ u ; v (\< pr u ; v \> ∈ G ⇔ ((\< pr u ; v \> ∈ f and u ∈ A and v ∈ B) or (u ∈ A and \< pr u ; b \> ∈ f and \< pr a ; v \> ∈ f))) ] and [ ∀ p ∈ G . [ ∃ u ; v \, p = \< pr u ; v \> ] ] ⟹ G ∈ A → B` / →.' [&l -| LGval || &r -| LGtot ,, LGuniq] v; LGI <- `a {/}∈ A and b {/}∈ B and f ∈ (A ∪ \{ set a \}) →I (B ∪ \{ set b \}) and [ ∀ u ; v (\< pr u ; v \> ∈ G ⇔ ((\< pr u ; v \> ∈ f and u ∈ A and v ∈ B) or (u ∈ A and \< pr u ; b \> ∈ f and \< pr a ; v \> ∈ f))) ] and [ ∀ p ∈ G . [ ∃ u ; v \, p = \< pr u ; v \> ] ] ⟹ G ∈ A →I B` -| LGmap ,, LGinj ,, →I.' v; LGex <- `f ∈ (A ∪ \{ set a \}) →I (B ∪ \{ set b \}) ⟹ [ ∃ G \, ([ ∀ u ; v (\< pr u ; v \> ∈ G ⇔ ((\< pr u ; v \> ∈ f and u ∈ A and v ∈ B) or (u ∈ A and \< pr u ; b \> ∈ f and \< pr a ; v \> ∈ f))) ] and [ ∀ p ∈ G . [ ∃ u ; v \, p = \< pr u ; v \> ] ]) ]` -| LGm ,, LGp v; Lpiece <- `a {/}∈ A and b {/}∈ B and f ∈ (A ∪ \{ set a \}) →I (B ∪ \{ set b \}) ⟹ [ ∃ h \, h ∈ A →I B ]` -| LGI ,, LGex v; Lsw / ≤#.' -| Lpiece p; Lsw -| W. h; !let/thm Lirr <- `n ∈ 𝕄 ⟹ n {/}∈ n` ◀ W. ,, ax_s prf Lirr -| <𝕄:l / ⊊.. p; Lirr -| W. ,, ax_s h; !let/thm PH <- `n ∈ 𝕄 ⟹ ¬ ( n suc ≤# n )` ◀ W. ,, ax_s prf A_ := `\{ cls n ∈ 𝕄 | ¬ ( n suc ≤# n ) \}` ; L0 <- `0 ∈ 𝕄` / 𝕄. -| O p; LE <- `[ ∃ A \, [ ∀ n (n ∈ A ⟺ n ∈ 𝕄 and ¬ ( n suc ≤# n )) ] ]` -| ax_s[C_:=`A_`] p; Lb <- `¬ ( 0 suc ≤# 0 )` / ≤#.' / →I.' / →.' -| suc.' ,, 0. ,, ∅.' p; Ls <- `n ∈ 𝕄 and ¬ ( n suc ≤# n ) ⟹ ¬ ( n suc suc ≤# n suc )` -| Lsw ,, suc. ,, Lirr ,, 𝕄1 p; LI <- `[ ∀ n (n ∈ A ⟺ n ∈ 𝕄 and ¬ ( n suc ≤# n )) ] ⟹ A ∈_ Ind` / ⊂. / ^suc. -| L0 ,, 𝕄1 ,, Lb ,, Ls p; LM <- `[ ∀ n (n ∈ A ⟺ n ∈ 𝕄 and ¬ ( n suc ≤# n )) ] ⟹ 𝕄 ⊂ A` -| LI ,, 𝕄. ,, ⊂. p; PH -| LE ,, LM ,, ⊂. p; PH -| W. ,, ax_s h; prop/thm Le_≤# ◀ W. ,, ax_s prf Lsucsub <- `[ m ; n col ∈ 𝕄 ] and n ∈ m ⟹ n suc ⊂ m` / ⊂. -| suc.' ,, <𝕄:l / ⊊.. / ⊂. p; Le_≤# -| <𝕄:T ,, <𝕄:r ,, ⊊.. ,, PH ,, sub_≤# ,, ≤#:RT ,, Lsucsub p; Le_≤# -| W. ,, ax_s h; !let/thm LextK <- `g ∈ D →I C and d {/}∈ D and C ⊂ Z and c ∈ Z and [ ∀ x \, \< pr x ; c \> {/}∈ g ] ⟹ g ∪ \{ set \< pr d ; c \> \} ∈ (D ∪ \{ set d \}) →I Z` ◀ W. prf K_ := `g ∪ \{ set \< pr d ; c \> \}` ; LKmem <- `[ ∀ u ; v (\< pr u ; v \> ∈ K_ ⇔ (\< pr u ; v \> ∈ g or (u = d and v = c))) ]` / ∪. / set1. -| pr:0 p; LKpair <- `g ∈ X → Y ⟹ [ ∀ p ∈ K_ . [ ∃ u ; v \, p = \< pr u ; v \> ] ]` / ∪. / set1. -| Lpair p; LKmap <- `g ∈ D →I C and d {/}∈ D and C ⊂ Z and c ∈ Z and [ ∀ u ; v (\< pr u ; v \> ∈ K ⇔ (\< pr u ; v \> ∈ g or (u = d and v = c))) ] and [ ∀ p ∈ K . [ ∃ u ; v \, p = \< pr u ; v \> ] ] ⟹ K ∈ (D ∪ \{ set d \}) → Z` / →.' -| Lfun ,, Lfval ,, Lfdom ,, Lftot ,, Lfuniq ,, LuD ,, ⊂. p; LKinj <- `g ∈ D →I C and [ ∀ x \, \< pr x ; c \> {/}∈ g ] and [ ∀ u ; v (\< pr u ; v \> ∈ K ⇔ (\< pr u ; v \> ∈ g or (u = d and v = c))) ] and \< pr x0 ; y \> ∈ K and \< pr x1 ; y \> ∈ K ⟹ x0 = x1` -| Lfinj p; LKI <- `g ∈ D →I C and d {/}∈ D and C ⊂ Z and c ∈ Z and [ ∀ x \, \< pr x ; c \> {/}∈ g ] and [ ∀ u ; v (\< pr u ; v \> ∈ K ⇔ (\< pr u ; v \> ∈ g or (u = d and v = c))) ] and [ ∀ p ∈ K . [ ∃ u ; v \, p = \< pr u ; v \> ] ] ⟹ K ∈ (D ∪ \{ set d \}) →I Z` -| LKmap ,, LKinj ,, →I.' v; LextK -| LKI ,, LKmem ,, LKpair ,, Lfun v; LextK -| W. h; subsection 有限集合と無限集合 !let/thm LIS_I <- `X =# Y ⟹ X ≤# Y` ◀ W. prf LIS_I / =#.' / ≤#.' -| →IS. ,, ∩. p; LIS_I -| W. h; !let/thm LB2 <- `[ m ; n col ∈ 𝕄 ] and m =# n ⟹ m = n` ◀ W. ,, ax_s prf LB2 -| Le_≤# ,, LIS_I ,, =#:RTX ,, =. ,, ⊂. p; LB2 -| W. ,, ax_s h; !let/thm INDS <- `0 ∈ B and [ ∀ m ∈ 𝕄 . (m ∈ B ⟹ m suc ∈ B) ] and n ∈ 𝕄 ⟹ n ∈ B` ◀ W. prf L0 <- `0 ∈ 𝕄` / 𝕄. -| O p; LI <- `0 ∈ B and [ ∀ m ∈ 𝕄 . (m ∈ B ⟹ m suc ∈ B) ] ⟹ 𝕄 ∩ B ∈_ Ind` / ⊂. / ^suc. / ∩. -| L0 ,, 𝕄1 p; LM <- `0 ∈ B and [ ∀ m ∈ 𝕄 . (m ∈ B ⟹ m suc ∈ B) ] ⟹ 𝕄 ⊂ 𝕄 ∩ B` -| LI ,, 𝕄. ,, ⊂. p; INDS -| LM ,, ⊂. ,, ∩. p; INDS -| W. h; !let/thm Lsucsub <- `n ⊂ n suc` ◀ W. prf Lsucsub / ⊂. -| suc.' p; Lsucsub -| W. h; !let/thm Lsucin <- `n ∈ n suc` ◀ W. prf Lsucin -| suc.' p; Lsucin -| W. h; !let/thm LB1 <- `[ chain Y =# k ∈ 𝕄 ] and a {/}∈ Y ⟹ Y ∪ \{ set a \} =# k suc` ◀ W. ,, ax_s prf Lnok <- `f ∈ Y → k and k ∈ 𝕄 ⟹ [ ∀ x \, \< pr x ; k \> {/}∈ f ]` -| Lfval ,, Lirr p; LB1i <- `f ∈ Y →I k and k ∈ 𝕄 and a {/}∈ Y ⟹ f ∪ \{ set \< pr a ; k \> \} ∈ (Y ∪ \{ set a \}) →I k suc` -| LextK ,, Lsucsub ,, Lsucin ,, Lnok ,, Lfun p; LB1s <- `f ∈ Y →S k and f ∪ \{ set \< pr a ; k \> \} ∈ (Y ∪ \{ set a \}) → k suc ⟹ f ∪ \{ set \< pr a ; k \> \} ∈ (Y ∪ \{ set a \}) →S k suc` / →S.' -| ∪. ,, set1. ,, suc.' ,, pr:0 p; LB1f <- `f ∈ Y →IS k and k ∈ 𝕄 and a {/}∈ Y ⟹ f ∪ \{ set \< pr a ; k \> \} ∈ (Y ∪ \{ set a \}) →IS k suc` / →IS. / ∩. -| LB1i ,, LB1s ,, Lfun p; LB1 / =#.' -| LB1f p; LB1 -| W. ,, ax_s h; !let/thm L0e <- `0 = ∅` ◀ W. prf L0e / =. -| 0.' ,, ∅. p; L0e -| W. h; newpage section 自然数の演算 subsection 加法 word + prop ^*+. prop *^+. prop ^^+. prop +𝕄 let/thm +∈𝕄 <- `[ m ; n col ∈ 𝕄 ] ⟹ m + n ∈ 𝕄` ◀ W. ,, ax_s ,, +𝕄 prf B_ := `\{ cls n ∈ 𝕄 | m + n ∈ 𝕄 \}` ; LBs <- `B_ ⊂_ 𝕄` -| O p; LBe <- `Exi B_` -| LBs ,, ax_s[C_:=`B_`] p; LBm <- `B =_ B_ ⟹ [ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and m + n ∈ 𝕄) ]` -| O p; L0 <- `0 ∈ 𝕄` / 𝕄. -| O p; LI <- `[ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and m + n ∈ 𝕄) ] and m ∈ 𝕄 and n ∈ 𝕄 ⟹ n ∈ B` -| L0 ,, +𝕄 ,, 𝕄1 ,, INDS p; +∈𝕄 -| LBe ,, LBm ,, LI p; +∈𝕄 -| W. ,, ax_s ,, +𝕄 h; !let/thm L×suc <- `\{ set c \} ^^pr (m suc) = (\{ set c \} ^^pr m) ∪ \{ set \< pr c ; m \> \}` ◀ W. prf L×suc / =. / ∪. / ^^pr. / set1. -| suc.' p; L×suc -| W. h; !let/thm L×0 <- `m ∈ 𝕄 ⟹ \{ set c \} ^^pr m =# m` ◀ W. ,, ax_s prf B_ := `\{ cls m ∈ 𝕄 | \{ set c \} ^^pr m =# m \}` ; LBs <- `B_ ⊂_ 𝕄` -| O p; LBe <- `Exi B_` -| LBs ,, ax_s[C_:=`B_`] p; LBm <- `B =_ B_ ⟹ [ ∀ m (m ∈ B ⟺ m ∈ 𝕄 and \{ set c \} ^^pr m =# m) ]` -| O p; L0 <- `0 ∈ 𝕄` / 𝕄. -| O p; Lb <- `\{ set c \} ^^pr 0 =# 0` -| =#0 ,, L0e ,, =. ,, ^^pr. ,, 0.' p; Lnin <- `m ∈ 𝕄 ⟹ \< pr c ; m \> {/}∈ \{ set c \} ^^pr m` / ^^pr. -| pr:0 ,, Lirr p; Ls <- `m ∈ 𝕄 and \{ set c \} ^^pr m =# m ⟹ \{ set c \} ^^pr (m suc) =# m suc` -| L×suc ,, Lnin ,, LB1 p; LI <- `[ ∀ m (m ∈ B ⟺ m ∈ 𝕄 and \{ set c \} ^^pr m =# m) ] and m ∈ 𝕄 ⟹ m ∈ B` -| L0 ,, Lb ,, Ls ,, 𝕄1 ,, INDS p; L×0 -| LBe ,, LBm ,, LI p; L×0 -| W. ,, ax_s h; !let/thm LDsuc <- `(\{ set c \} ^^pr m) ∪ (\{ set d \} ^^pr n suc) = ((\{ set c \} ^^pr m) ∪ (\{ set d \} ^^pr n)) ∪ \{ set \< pr d ; n \> \}` ◀ W. prf LDsuc / =. -| L×suc ,, ∪. p; LDsuc -| W. h; !let/thm LD0 <- `(\{ set c \} ^^pr m) ∪ (\{ set d \} ^^pr 0) = \{ set c \} ^^pr m` ◀ W. prf LD0 / =. / ∪. / ^^pr. -| 0.' p; LD0 -| W. h; !let/thm LDnin <- `c {/}= d and n ∈ 𝕄 ⟹ \< pr d ; n \> {/}∈ (\{ set c \} ^^pr m) ∪ (\{ set d \} ^^pr n)` ◀ W. ,, ax_s prf LDnin / ∪. / ^^pr. / set1. -| pr:0 ,, Lirr p; LDnin -| W. ,, ax_s h; !let/thm +=#g <- `c {/}= d and [ m ; n col ∈ 𝕄 ] ⟹ m + n =# (\{ set c \} ^^pr m) ∪ (\{ set d \} ^^pr n)` ◀ W. ,, ax_s ,, +𝕄 prf B_ := `\{ cls n ∈ 𝕄 | (\{ set c \} ^^pr m) ∪ (\{ set d \} ^^pr n) =# m + n \}` ; LBs <- `B_ ⊂_ 𝕄` -| O p; LBe <- `Exi B_` -| LBs ,, ax_s[C_:=`B_`] p; LBm <- `B =_ B_ ⟹ [ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and (\{ set c \} ^^pr m) ∪ (\{ set d \} ^^pr n) =# m + n) ]` -| O p; L0 <- `0 ∈ 𝕄` / 𝕄. -| O p; Lb <- `m ∈ 𝕄 ⟹ (\{ set c \} ^^pr m) ∪ (\{ set d \} ^^pr 0) =# m + 0` -| LD0 ,, L×0 ,, +𝕄 p; Ls <- `c {/}= d and [ m ; n col ∈ 𝕄 ] and (\{ set c \} ^^pr m) ∪ (\{ set d \} ^^pr n) =# m + n ⟹ (\{ set c \} ^^pr m) ∪ (\{ set d \} ^^pr n suc) =# m + n suc` -| LDsuc ,, LDnin ,, LB1 ,, +∈𝕄 ,, +𝕄 p; LI <- `[ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and (\{ set c \} ^^pr m) ∪ (\{ set d \} ^^pr n) =# m + n) ] and c {/}= d and m ∈ 𝕄 and n ∈ 𝕄 ⟹ n ∈ B` -| L0 ,, Lb ,, Ls ,, 𝕄1 ,, INDS p; +=#g -| LBe ,, LBm ,, LI ,, =#:X v; +=#g -| W. ,, ax_s ,, +𝕄 h; let/thm +=# <- `[ m ; n col ∈ 𝕄 ] ⟹ m + n =# (\{ set 0 \} ^^pr m) ∪ (\{ set 1 \} ^^pr n)` ◀ W. ,, ax_s ,, +𝕄 prf +=# -| +=#g ,, ≠2 p; +=# -| W. ,, ax_s ,, +𝕄 h; let/thm +:C <- `[ m ; n col ∈ 𝕄 ] ⟹ m + n = n + m` ◀ W. ,, ax_s ,, +𝕄 prf L1 <- `[ m ; n col ∈ 𝕄 ] ⟹ n + m =# (\{ set 1 \} ^^pr n) ∪ (\{ set 0 \} ^^pr m)` -| +=#g ,, ≠2 p; L2 <- `(\{ set 1 \} ^^pr n) ∪ (\{ set 0 \} ^^pr m) = (\{ set 0 \} ^^pr m) ∪ (\{ set 1 \} ^^pr n)` / =. / ∪. -| O p; L3 <- `[ m ; n col ∈ 𝕄 ] ⟹ m + n =# n + m` -| +=# ,, L1 ,, L2 ,, =#:RTX p; +:C -| L3 ,, LB2 ,, +∈𝕄 p; +:C -| W. ,, ax_s ,, +𝕄 h; subsection 乗法 word ⋅ prop ^**. prop *^*. prop ^^*. prop *𝕄 let/thm ⋅∈𝕄 <- `[ m ; n col ∈ 𝕄 ] ⟹ m ⋅ n ∈ 𝕄` ◀ W. ,, ax_s ,, +𝕄 ,, *𝕄 prf B_ := `\{ cls n ∈ 𝕄 | m ⋅ n ∈ 𝕄 \}` ; LBs <- `B_ ⊂_ 𝕄` -| O p; LBe <- `Exi B_` -| LBs ,, ax_s[C_:=`B_`] p; LBm <- `B =_ B_ ⟹ [ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and m ⋅ n ∈ 𝕄) ]` -| O p; L0 <- `0 ∈ 𝕄` / 𝕄. -| O p; Lb <- `m ∈ 𝕄 ⟹ m ⋅ 0 ∈ 𝕄` -| L0 ,, *𝕄 p; Ls <- `[ m ; n col ∈ 𝕄 ] and m ⋅ n ∈ 𝕄 ⟹ m ⋅ (n suc) ∈ 𝕄` -| *𝕄 ,, +∈𝕄 p; LI <- `[ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and m ⋅ n ∈ 𝕄) ] and m ∈ 𝕄 and n ∈ 𝕄 ⟹ n ∈ B` -| L0 ,, Lb ,, Ls ,, 𝕄1 ,, INDS p; ⋅∈𝕄 -| LBe ,, LBm ,, LI p; ⋅∈𝕄 -| W. ,, ax_s ,, +𝕄 ,, *𝕄 h; newpage section 部分集合の個数 txt 自然数の冪 \(m^n\) を表す word を紹介します。加法・乗法と同じく、定義はせず、性質 ↑𝕄 を仮定として使います。 word* ↑ prop ↑𝕄 <- `\\{ And m ∈ 𝕄 ⟹ m ↑ 0 = 1 \\ [ m ; n col ∈ 𝕄 ] ⟹ m ↑ { n suc } = (m ↑ n) ⋅ m \\}` !let/thm L1∈𝕄 <- `1 ∈ 𝕄` ◀ W. prf L0 <- `0 ∈ 𝕄` / 𝕄. -| O p; L1∈𝕄 -| L0 ,, 𝕄1 ,, 1.. p; L1∈𝕄 -| W. h; !let/thm L2∈𝕄 <- `2 ∈ 𝕄` ◀ W. prf L2∈𝕄 -| L1∈𝕄 ,, 𝕄1 ,, 2.. p; L2∈𝕄 -| W. h; !let/thm ↑∈𝕄 <- `[ m ; n col ∈ 𝕄 ] ⟹ m ↑ n ∈ 𝕄` ◀ W. ,, ax_s ,, +𝕄 ,, *𝕄 ,, ↑𝕄 prf B_ := `\{ cls n ∈ 𝕄 | m ↑ n ∈ 𝕄 \}` ; LBs <- `B_ ⊂_ 𝕄` -| O p; LBe <- `Exi B_` -| LBs ,, ax_s[C_:=`B_`] p; LBm <- `B =_ B_ ⟹ [ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and m ↑ n ∈ 𝕄) ]` -| O p; L0 <- `0 ∈ 𝕄` / 𝕄. -| O p; Lb <- `m ∈ 𝕄 ⟹ m ↑ 0 ∈ 𝕄` -| L1∈𝕄 ,, ↑𝕄 p; Ls <- `[ m ; n col ∈ 𝕄 ] and m ↑ n ∈ 𝕄 ⟹ m ↑ { n suc } ∈ 𝕄` -| ↑𝕄 ,, ⋅∈𝕄 p; LI <- `[ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and m ↑ n ∈ 𝕄) ] and m ∈ 𝕄 and n ∈ 𝕄 ⟹ n ∈ B` -| L0 ,, Lb ,, Ls ,, 𝕄1 ,, INDS p; ↑∈𝕄 -| LBe ,, LBm ,, LI p; ↑∈𝕄 -| W. ,, ax_s ,, +𝕄 ,, *𝕄 ,, ↑𝕄 h; !let/thm L⋅2 <- `m ∈ 𝕄 ⟹ m ⋅ 2 = m + m` ◀ W. ,, ax_s ,, +𝕄 ,, *𝕄 prf L0 <- `0 ∈ 𝕄` / 𝕄. -| O p; L0+ <- `m ∈ 𝕄 ⟹ 0 + m = m` -| +:C ,, +𝕄 ,, L0 p; L⋅2 -| *𝕄 ,, L0+ ,, 1.. ,, 2.. ,, L0 ,, L1∈𝕄 p; L⋅2 -| W. ,, ax_s ,, +𝕄 ,, *𝕄 h; !let/thm L2u <- `2 ^^pr m = (\{ set 0 \} ^^pr m) ∪ (\{ set 1 \} ^^pr m)` ◀ W. prf L2u / =. / ∪. / ^^pr. / set1. -| 2. ,, pr:0 p; L2u -| W. h; !let/thm L+2 <- `m ∈ 𝕄 ⟹ m + m =# 2 ^^pr m` ◀ W. ,, ax_s ,, +𝕄 prf L+2 -| +=# ,, L2u p; L+2 -| W. ,, ax_s ,, +𝕄 h; !let/thm L2× <- `X =# Y ⟹ 2 ^^pr X =# 2 ^^pr Y` ◀ W. ,, ax_s prf G_ := `\{ \< pr \< pr i ; x \> ; \< pr i ; y \> \> Cls i ; x ; y | i ∈ 2 and \< pr x ; y \> ∈ f \}` ; LGs <- `f ∈ X →IS Y ⟹ G_ ⊂_ (2 ^^pr X) ^^pr (2 ^^pr Y)` / →IS.' / →.' // ^^pr. -| pr:0 p; LGe <- `f ∈ X →IS Y ⟹ Exi G_` -| LGs ,, ax_s[C_:=`G_`] v; LGf <- `f ∈ X →IS Y and G =_ G_ ⟹ G ∈ (2 ^^pr X) → (2 ^^pr Y)` / →IS.' / →.' // ^^pr. -| pr:0 p; LGS <- `f ∈ X →IS Y and G =_ G_ ⟹ [ ∀ q ∈ 2 ^^pr Y . [ ∃！ p \< pr p ; q \> ∈ G ] ]` / →IS.' / →.' // ^^pr. -| pr:0 p; LGIS <- `f ∈ X →IS Y and G =_ G_ ⟹ G ∈ (2 ^^pr X) →IS (2 ^^pr Y)` /2 →IS.' -| LGf ,, LGS p; L2× / =#.' -| LGIS ,, LGe v; L2× -| W. ,, ax_s h; !let/thm L℘suc <- `n ∈ 𝕄 ⟹ 2 ^^pr ℘ n =# ℘ (n suc)` ◀ W. ,, ax_s prf H_ := `\{ \< pr \< pr i ; A \> ; B \> Cls i ; A ; B | A ⊂ n and ((i = 0 and B = A) or (i = 1 and B = A ∪ \{ set n \})) \}` ; LHs <- `H_ ⊂_ (2 ^^pr ℘ n) ^^pr ℘ (n suc)` // ^^pr. / ℘. / ⊂. -| 2. ,, suc.' ,, ∪. ,, set1. ,, pr:0 v; LHe <- `Exi H_` -| LHs ,, ax_s[C_:=`H_`] v; LB <- `B ⊂ n suc ⟹ B ∩ n ⊂ n and (n ∈ B ⟹ B = (B ∩ n) ∪ \{ set n \}) and (n {/}∈ B ⟹ B = B ∩ n)` / ⊂. / =. / ∪. / ∩. / set1. -| suc.' p; LHa <- `H =_ H_ ⟹ [ ∀ w ∈ H . [ ∃ p ∈ 2 ^^pr ℘ n . [ ∃ B ∈ ℘ (n suc) . w = \< pr p ; B \> ] ] ]` // ^^pr. / ℘. / ⊂. -| 2. ,, suc.' ,, ∪. ,, set1. ,, pr:0 v; LHt <- `H =_ H_ ⟹ [ ∀ p ∈ 2 ^^pr ℘ n . [ ∃ B \< pr p ; B \> ∈ H ] ]` / ^^pr. / ℘. -| 2. ,, pr:0 p; LHu <- `H =_ H_ and \< pr p ; B \> ∈ H and \< pr p ; C \> ∈ H ⟹ B = C` -| pr:0 ,, ≠2 p; LHf <- `H =_ H_ ⟹ H ∈ (2 ^^pr ℘ n) → ℘ (n suc)` / →.' -| LHa ,, LHt ,, LHu v; LHsur <- `H =_ H_ and B ⊂ n suc ⟹ [ ∃ p \< pr p ; B \> ∈ H ]` -| LB ,, 2. p; LJ1 <- `n ∈ 𝕄 and A ⊂ n ⟹ n {/}∈ A` / ⊂. -| Lirr p; LJ2 <- `n {/}∈ A and n {/}∈ C and A ∪ \{ set n \} = C ∪ \{ set n \} ⟹ A = C` / =. / ∪. / set1. -| O p; LJ3 <- `n {/}∈ C ⟹ A ∪ \{ set n \} {/}= C` -| ∪. ,, set1. p; LHinj <- `n ∈ 𝕄 and H =_ H_ and \< pr p ; B \> ∈ H and \< pr q ; B \> ∈ H ⟹ p = q` -| pr:0 ,, ≠2 ,, LJ1 ,, LJ2 ,, LJ3 v; LHS <- `n ∈ 𝕄 and H =_ H_ ⟹ [ ∀ B ∈ ℘ (n suc) . [ ∃！ p \< pr p ; B \> ∈ H ] ]` / ℘. -| LHsur ,, LHinj v; LHIS <- `n ∈ 𝕄 and H =_ H_ ⟹ H ∈ (2 ^^pr ℘ n) →IS ℘ (n suc)` /2 →IS.' -| LHf ,, LHS v; L℘suc / =#.' -| LHIS ,, LHe v; L℘suc -| W. ,, ax_s h; txt 有限集合 \(n\) の部分集合全体の濃度は \(2^n\) です（No 52）。 thm `n ∈ 𝕄 ⟹ ℘ n =# 2 ↑ n` ◀ W. ,, ax_s ,, +𝕄 ,, *𝕄 ,, ↑𝕄 prf B_ := `\{ cls n ∈ 𝕄 | ℘ n =# 2 ↑ n \}` ; LBs <- `B_ ⊂_ 𝕄` -| O p; LBe <- `Exi B_` -| LBs ,, ax_s[C_:=`B_`] p; LBm <- `B =_ B_ ⟹ [ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and ℘ n =# 2 ↑ n) ]` -| O p; L0 <- `0 ∈ 𝕄` / 𝕄. -| O p; Lb <- `℘ 0 =# 2 ↑ 0` -| ↑𝕄 ,, L2∈𝕄 ,, =#1 ,, ℘. ,, ⊂. ,, L0e ,, ∅. ,, =. ,, set1. v; Ls <- `n ∈ 𝕄 and ℘ n =# 2 ↑ n ⟹ ℘ (n suc) =# 2 ↑ { n suc }` -| L℘suc ,, L2× ,, L+2 ,, L⋅2 ,, ↑𝕄 ,, ↑∈𝕄 ,, L2∈𝕄 ,, =#:RTX p; LI <- `[ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and ℘ n =# 2 ↑ n) ] and n ∈ 𝕄 ⟹ n ∈ B` -| L0 ,, Lb ,, Ls ,, 𝕄1 ,, INDS p; goal -| LBe ,, LBm ,, LI p; goal -| W. ,, ax_s ,, +𝕄 ,, *𝕄 ,, ↑𝕄 h;
表示（保存しません）
保存にはMatheliaへのログインが要ります。