Mizar/本体部/定義式

⇔

A means B;

---

定義中のラベルは :～: で表す。

※abstractファイルを作る場合には、 定義のラベルは

def数字

定理のラベルは

数字

となります。

---

と等しい≡

y equals :ラベル名: 2*x;

置く⇒

x*y -> set means :A2: z;

正の値をもつ

x is positive means :A3: 0<x;

---

置換