Mizar/本体部/証明したい式
述語論理記法で表記する
域 演算 性質 proof ....
∀x ∃y f(x)=a → g(x)=h(y) ----------------------------------------------------------------- 理解しやすいように括弧でくくると ((∀x)(∃y)) (f(x)=a → g(x)=h(y)) ----------------------------------------------------------------- 関係式をより分かりやすくする ((∀x)(∃y))∋(f(x)=a → g(x)=h(y)) ----------------------------------------------------------------- Mizarの述語論理記法 for x ex y st f[x]=a holds g[x]=h[x]; ----------------------------------------------------------------- 以上の要領で以下のようにも記述できる ∀x,y ∃t x(t)⇔y(t) for x,y ex t st x(t) iff y(t)
| 数学記号 | 記号名 | Mizar | 意味 |
| ∀ | 全称記号 | for | (for, any)広がりを持った空間 |
| ∃ | 存在記号 | ex | (existence , being)限定された空間(点など) |
| →,⊂,⊆ | holds | 成り立つと | |
| ∧ | and | & | かつ |
| ∨ | or | or | または |
| ￢ | not | not | でない |
| ＝ | = | = | 等しい |
| ⇔ | 同値 | iff | if and only if |
| ⇒ | ならば | implies | ならば |
| ∈ | <- | ||
| ：，∈ | such that | ||
| ⊆ | c= |