example
差分
このページの2つのバージョン間の差分を表示します。
| 両方とも前のリビジョン前のリビジョン次のリビジョン | 前のリビジョン | ||
| example [2025/04/08 02:45] – superuser | example [2025/05/29 06:35] (現在) – superuser | ||
|---|---|---|---|
| 行 1: | 行 1: | ||
| ====== 第1章 TARSKIの公理系 ====== | ====== 第1章 TARSKIの公理系 ====== | ||
| - | このテキストは，集合論を題材に，mizar を使った，数学定理の記述が，実際にどのようになされているかを説明します。 | + | このテキストは集合論を題材に mizar を使った数学定理の記述が実際にどのようになされているかを説明します。 |
| mizar では，その数学記述言語によって書かれたテキストを **articles** と称します。 | mizar では，その数学記述言語によって書かれたテキストを **articles** と称します。 | ||
| mizar システムやそれで使われる数学記述言語の文法については，中村八束教授著の mizar 講義録第３版 | mizar システムやそれで使われる数学記述言語の文法については，中村八束教授著の mizar 講義録第３版 | ||
| 行 233: | 行 233: | ||
| <mizar ta> | <mizar ta> | ||
| scheme Replacement{ A() -> set, P[object, | scheme Replacement{ A() -> set, P[object, | ||
| - | ex X st for x being object holds x in X iff | + | ex X st for x being object holds x in X |
| - | ex y being object st y in A() & P[y,x] | + | |
| provided | provided | ||
| A1: for x,y,z being object st P[x,y] & P[x,z] holds y = z | A1: for x,y,z being object st P[x,y] & P[x,z] holds y = z | ||
example.1744080341.txt.gz · 最終更新: by superuser