Mizar/本体部/定義式

出典: フリー教科書『ウィキブックス(Wikibooks)』

A means B;

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

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

def数字

定理のラベルは

数字

となります。


と等しい≡

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

置く⇒

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

正の値をもつ

x is positive means :A3: 0<x;

置換