コンテンツにスキップ

Mizar/本体部/関係演算子

出典: フリー教科書『ウィキブックス(Wikibooks)』
成り立つ
A
A holds

A → B
A holds B

階層的に考えると{A{B}}
関数的に考えるとB(A)
Aという定義域が成立すると、Bという値域をもつ。
A ⇒ B
A implies B
A ⇔ B
A iff B

※if and only if ≡ iff