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=    

数学証明

数学記号