Mizar/本体部/証明

証明の形式、骨組み：(スケルトン)

[論理式] proof [証明法] end;

Aが成立する
--------------------------------------------------
proof
 thus A;
end;

Q⇒A
 Qを仮定する
  ～
 Aとなる
--------------------------------------------------
Q implies A
proof
 assume Q;
  ～
 thus A;
end;

given = assume　+ consider とする場合
((∃x)Q[x})⇒A
 xをQ[x}に与える
  ～
Aとなる
--------------------------------------------------
(ex x st Q[x]) implies A
 proof
  given x such that Q[x];
  ······
  ～
  ······
  thus A;
 end;

A⇔B
 A⇒B
 and
 B⇒A
--------------------------------------------------
A iff B
proof
 thus A implies B;
 thus B implies A;
end;
==================================================
A⇔B
 これにより
  Aを仮定
  Bとなる
 Bを仮定
 Aとなる
--------------------------------------------------
A iff B
proof
 hereby
  assume A;
  thus B;
 end;
 assume B;
 thus A;
end;

A or B
Aでないと仮定
Bとなる
---------------------------------------------------
A or B
proof
 assume not A;
 thus B;
end;

A and B
Aが成立
Bが成立
---------------------------------------------------
A & B
proof
 thus A;
 thus B;
end;

∀ x ∈集合  ⊆  f(x)
 x∈集合
 f(x)が成立
---------------------------------------------------
for x being set holds f(x)
proof
 let x be set;
 thus f(x);
end;

∃ x ∈集合  ⇒  f(x)
 あるxとする
 f(x)が成立
---------------------------------------------------
ex x being set st f(x)
proof
 take a;
 thus f(a);
end;

Pは正しい
 Pは間違っていると仮定する
 矛盾する

Qは間違っている
 Qは間違っていると仮定する
 矛盾しない

A⇒B and B⇒C

A⇒B or A⇒C

consider 変数 型;

変数rを再定義する場合には

reconsider 変数 型;

ラベル付けを行う。(同じラベルの場合には直前のラベルが引用される)

ラベル名:式;

A1: a=b;

that ラベル：式

such that ラベル：式

assume 仮定式