Mizar/本体部/証明したい式
(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= |