論理

命題論理

述語論理

集合

集合

数学で扱う対象の集まりを集合といい,その集合を構成する対象を元,要素と言う.集合\( A \)に要素\( a \)が属するとき, \[ a \in A \] と表す.

公理

数学で,無条件で認める仮定を公理と言う. 形式体系での集合論は通常ZFC公理系で以下を公理として認める.

外延性公理

集合の等しさを定める. 同じ要素で構成されるならその集合は等しい \[ \forall A \forall B (\forall x ( x \in A \leftrightarrow x \in B)) \to A = B \]

集合の定義

集合を定義するのに,その集合に属する要素をすべて並べる外延的記法と その集合に属するために必要な論理的条件にて,それに属する要素を定める内包的記法がある.

外延的記法

以下のように,10より小さい自然数で偶数の集合を列挙して書く. \[ \{ 2,4,6,8 \} \]

内包的記法

以下のように,10より小さい自然数で偶数の集合を条件にて提示する \[ \{ x | x < 0 \land x=2n, n \in \mathbb{N} \} \]

集合の演算

写像

写像

写像

2つの集合の\(X,Y\)の要素\( \forall x \in X, \forall y \in Y \)において,\(x\)に\(y\)を唯一つ対応させる写像(関数)\(f\)を \[ f: X \mapsto Y \] で定義する.\(X\)を定義域,\(Y\)を値域という. \[ y = f(x) \] と書いたとき,\(y\)を\(f\)による\(x\)の値という. \(A \subset X, B \subset Y\)のとき \[ B = f(A) \] ならば,\(B\)を\(f(A)\)の像という.

逆写像

\[ f: X \mapsto Y \] で定義された写像に対して,\(\forall B \subset Y\)としたとき, \[ f^{-1}(B) := \{x \in X| f(x) \in B \} \] を\(B\)による

Coq

Coqでの古典集合

mathcomp

外包的記法

Inductive Fruits : Type :=
| Apple
| Orange
| PineApple
| Mango.

内包的記法

  Definition IsMyFruits (fruits : Fruits) : Prop :=
    match fruits with
    | Apple => True
    | Orange => True
    | Mango => True
    | _ => False
    end.

写像

写像

\( f(A \cup B) = f(A) \cup f(B) \)

Lemma image_setU f A B : f @` (A `|` B) = f @` A `|` f @` B.

\( f(A \cap B) \subset f(A) \cap f(B) \)

Lemma sub_image_setI f A B : f @` (A `&` B) `<=` f @` A `&` f @` B.

\( A \subset f^{-1}(A) \)

Lemma preimage_image f A : A `<=` f @^-1` (f @` A).