Mizar/本体部/定義式
（Mizar/本体部/置換法 から転送）
⇔
A means B;
定義中のラベルは :～: で表す。
※abstractファイルを作る場合には、 定義のラベルは
- def数字
定理のラベルは
- 数字
となります。
と等しい≡
y equals :ラベル名: 2*x;
置く⇒
x*y -> set means :A2: z;
正の値をもつ
x is positive means :A3: 0<x;
⇔
A means B;
定義中のラベルは :～: で表す。
※abstractファイルを作る場合には、 定義のラベルは
定理のラベルは
となります。
と等しい≡
y equals :ラベル名: 2*x;
置く⇒
x*y -> set means :A2: z;
正の値をもつ
x is positive means :A3: 0<x;