i, j, k, l, m, n は 自然 数 とする。 このとき i + k = j + k ならば i = j 証明: まず 述語を定義する: P[自然 数] とは i + $1 = j + $1 ならば i=j であること。 (A1): P[0] ※帰納法のベース 証明: 次を仮定する: (B0): i + 0 = j + 0 。 このとき (B1)…

http://fm.mizar.org/contents.html より： Title: Tarski Grothendieck Set Theory Author: Andrzej Trybulec Year: 1990 Identifier: TARSKI PDF URL: http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf Summary: This is the first part of the axiomatics o…

名前がないからどうにもならないが、名無し／メタ情報なしでも、 特定シンボル（述語名、関数名、モード名、属性名）を含む定理 特定のプロファイルの特定のシンボルを含む定理 特定のアーティクルで定義された特定のシンボルを含む定理 存在命題、全称命題…

http://www.chimaira.org/archive/MizarLightForHOLLight_miz.ps.pdf より、 :: The drinker's principle reserve x for object; ex x st P x implies for y holds P y proof per cases; suppose A0: ex x st not P x; consider a such that A1: not P a by …

the system Declare by D. Syme ？？ 不明 the Mizar mode for HOL by J.Harrison http://www.cl.cam.ac.uk/~jrh13/papers/mizar.html the Isar language for Isabelle by M. Wenzel http://isabelle.in.tum.de/Isar/ Mizar-light for HOLlight by F. Wiedij…

地獄の作業例。 reserve i,j,k,l,m,n for natural number; i+k = j+k implies i=j; proof defpred P[natural number] means i+$1 = j+$1 implies i=j; A1: P[0] proof assume B0: i+0 = j+0; B1: i+0 = i by INDUCT:3; B2: j+0 = j by INDUCT:3; hence thesi…

論理 Mizar ⊥ contradiction ¬φ not φ φ ∧ ψ φ & ψ φ ∨ ψ φ or ψ φ ⇒ ψ φ implies ψ φ ⇔ ψ φ iff ψ ∃ x. ψ ex x st ψ ∀ x. ψ for x holds ψ ∀ x.(φ ⇒ ψ) for x st φ holds ψ nonは形容詞の否定、andとsuch thatはスクリプト言語のキーワード。

Mizarでは同義語はほとんどない。beとbeing, hence（従って）、hereby（これによって）が次の意味。 then + thus = hence thus + now = hereby 英語としてはthus（よって）とhence（従って）はたいして差はない。

連続 離散二値 R, C B 可換環（スカラー） ベキ等可換半環 空間S 単なる集合X 確率分布 ポッシビリティ分布 S上の状態ベクトル空間 Xのベキ集合に合併 バンドル 依存和 バンドルのセクション空間 依存積集合 連続群 モノイド 群代数 モノイドのベキ集合 群代…

Frobenius algebras and monoidal categories Ross Street Annual Meeting Aust. Math. Soc. September 2004 http://maths.mq.edu.au/~street/FAMC.pdf フロベニウス代数の圏でも、ニョロニョロは成立して、それによりフロベニウス代数射が可逆であることが…

ネーミングの選択が難しいのだが、 N値の1-形式＝1-コチェインが問題。一応C1(A, N)でN値の形式＝コチェインを表す。 三角ハイブ上で1-コサイクルを考えることが出来る。コバウンダリ作用素がないが、それでも等式で定義できる。コサイクルが許容状態（addmi…

吸い込み部屋と湧き出し部屋を禁止してるが、許しても議論はできる。ただし、直感性は失われるし、ややこしくなる。許した場合は、乗法と余単位、単位と余乗法の相互関係が必要になるし、そもそもこの相互関係はフロベニウス代数の公理系に入れてもいいもの…

任意の曲面上の三角ハイブ理論は思ったよりも難しい。難しい理由は双対グラフが平面グラフにならないので、平面に射影すると交差が出てきてしまい、その操作に、ブレイド圏や対称圏の議論を必要とする。三角ハイブが最初から平面に埋め込まれていれば、ブレ…