未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
freek100/74.book
ヘッダ
行番号
title 数学的帰納法 formel /common/default thmel /common/zf option review quick:true;
section 一階述語論理 subsection 通常の論理記号 word and or ⇒ ⇔ word ∀ ∃ word = word =_ subsection 高度な論理記号 word ⟹ ⟺ lower ⟹ lower ⟺ subsection 量化子の略記法 abbr ∀ abbr ∃ abbr ∀+ abbr ∃+ newpage section 基本記号① subsection 所属関係と内包記法 word ∈ word ∈_ word \cls abbr cls abbr cls+ subsection 外延性 prop =_. prop =. subsection 包含関係 word ⊂_ prop ⊂_. word ⊂ prop ⊂. newpage section 集合・クラスの最初の例 subsection 有限集合 word set\n abbr set prop set\n. subsection 合併、共通部分、差 word ∪_ prop ∪_. word ∪ prop ∪. subsection 総合併、総共通部分 word ⋂_ prop ⋂_. newpage section 基本記号② subsection 一意量化子 abbr ！ subsection 集合となるクラス word Exi prop Exi. 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 subsection 関数の像 word {^} lower {^} newpage section 自然数 subsection 0と後続関数 word 0 word suc ^suc prop suc. !prop/thm suc.' ◀ W. prf suc.' // W.!=. -| O p; suc.' -| W. h; prop ^suc. subsection 帰納法 word Ind prop Ind. word 𝕄 prop 𝕄. !prop/thm 𝕄1 ◀ W. prf 𝕄1 /// W.'!=. -| O p; 𝕄1 -| W. h; newpage section 数学的帰納法 txt 自然数についての性質 \(P\) が \(0\) で成り立ち、\(n\) で成り立てば \(n\) の後者でも成り立つならば、\(P\) はすべての自然数で成り立ちます。 thm `?p^ 0 and [ ∀ n ∈ 𝕄 . ?p^ n ⟹ ?p^ (n suc) ] ⟹ [ ∀ n ∈ 𝕄 . ?p^ n ]` ◀ W. ,, ax_s prf A_ := `\{ cls m ∈ 𝕄 | ?p^ m \}` ; LAs <- `A_ ⊂_ 𝕄` /// W. -| O p; LEA <- `Exi A_` -| LAs ,, ax_s[C_:=`A_`] p; LE <- `[ ∃ A \, [ ∀ m (m ∈ A ⟺ m ∈ 𝕄 and ?p^ m) ] ]` -| LEA p; LI <- `?p^ 0 and [ ∀ n ∈ 𝕄 . ?p^ n ⟹ ?p^ (n suc) ] and [ ∀ m (m ∈ A ⟺ m ∈ 𝕄 and ?p^ m) ] ⟹ A ∈_ Ind` / ⊂. / ^suc. -| 𝕄1 ,, 𝕄. p; LM <- `?p^ 0 and [ ∀ n ∈ 𝕄 . ?p^ n ⟹ ?p^ (n suc) ] and [ ∀ m (m ∈ A ⟺ m ∈ 𝕄 and ?p^ m) ] ⟹ 𝕄 ⊂ A` -| LI ,, 𝕄. ,, ⊂. v; goal -| LE ,, LM ,, ⊂. p; goal -| W. ,, ax_s h;
表示（保存しません）
保存にはMatheliaへのログインが要ります。