|
|
数学記号 |
|
|
|
|
意味 |
|
説明 |
[Tex] |
[mizar] |
定義ファイル |
|
[Mizar]使用法 |
使用法の意味
|
|
|
数学記号 |
|
|
|
|
意味 |
|
説明 |
[Tex] |
[mizar] |
定義ファイル |
|
Mizar使用法[usage] |
[usage]使用法意味 |
|
| 1 |
0 |
＜Logical notations＞ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 1 |
1 |
￢ |
|
|
|
|
negation |
否定 |
「￢P」は「命題 P が偽」という命題を表す。 |
\neg |
not |
(build in Mizar system) |
|
not P |
[not P] |
|
| 1 |
1.1 |
￣ |
|
|
|
|
negation |
否定 |
|
\bar{P} |
not |
(build in Mizar system) |
|
not P |
[not P] |
|
| 1 |
1.2 |
～ |
|
|
|
|
negation |
否定 |
|
|
not |
(build in Mizar system) |
|
not P |
[not P] |
|
| 1 |
2 |
∧ |
& |
|
|
|
and (conjunction) |
論理積 |
「A ∧ B」は「命題 A と命題 B がともに真」という命題を表す。 |
\wedge |
& |
(build in Mizar system) |
|
A & B |
[A and B] |
|
| 1 |
3 |
∨ |
|
|
|
|
or (disjunction) |
論理和 |
「A ∨ B」は「命題 A と命題 B の少なくとも一方は真」という命題を表す。 |
\vee |
or |
(build in Mizar system) |
|
A or B |
[A or B] |
|
| 1 |
4 |
→ |
⇒ |
⊂ |
⊆ |
|
implication |
論理包含、導出 |
「A ⇒ B」は、「命題 A が真なら必ず命題 B も真」という命題を表す。A が偽の場合は A ⇒ B は真であることに注意が必要。 |
\Rightarrow |
implies |
(build in Mizar system) |
|
A implies B |
[A implies B] |
|
| 1 |
4.1 |
⊂ |
⊆ |
|
|
|
holds |
論理包含 |
「A⊂B」と「A ⇒ B」,「￢A∨B」は同値である |
\subseteqq \subset |
holds |
(build in Mizar system) |
|
A holds B |
[A holds B] |
|
| 1 |
5 |
⇔ |
|
|
|
|
equivalence |
同値 |
「A ⇔ B」は A と B の真偽が必ず一致することを意味する。 |
\Leftrightarrow |
iff |
(build in Mizar system) |
|
A iff B |
[A is equivalent to B] |
|
| 1 |
6 |
∀ |
|
|
|
|
for all |
全称限量記号 |
しばしば ∀ x ∈ S; P(x) のように書かれ、集合 S の任意の元 x に対して命題 P(x) が成立することを表す。 |
\forall |
for |
(build in Mizar system) |
1 |
for a holds P |
[for every a, P holds.] |
|
| 1 |
6.1 |
|
|
|
|
|
|
|
|
|
|
|
2 |
for a being set holds P |
[For every a which is a set, P holds.] |
|
| 1 |
6.2 |
|
|
|
|
|
|
|
|
|
|
|
3 |
for a, b being set holds P |
[For every a, b which are sets, P holds.] |
|
| 1 |
6.3 |
|
|
|
|
|
|
|
|
|
|
|
4 |
for a being set st P holds Q |
[For every set a satisfied with P, Q holds.] |
|
| 1 |
7 |
∃ |
|
|
|
|
there exists |
存在限量記号 |
しばしば ∃ x ∈ S; P(x) のように書かれ、集合 S の中に命題 P(x) を成立させるような元 x が少なくとも1つ存在することを表す。 |
\exists |
ex |
(build in Mizar system) |
1 |
ex a |
[There exists a.] |
|
| 1 |
7.1 |
|
|
|
|
|
|
|
|
|
|
|
2 |
ex a st P |
[There exists a such that P holds.] |
|
| 1 |
7.2 |
|
|
|
|
|
|
|
|
|
|
|
3 |
ex a being set st P |
[There exists a set a such that P holds.] |
|
| 1 |
7.3 |
∃1 |
∃! |
|
|
|
|
一意的に存在 |
しばしば ∃1 x ∈ S; P(x) のように書かれ、集合 S の中に命題 P(x) を成立させるような元 x が唯1つ存在することを表す。 |
|
|
|
|
|
|
|
| 1 |
8 |
T |
t |
true |
TRUE |
1 |
truth |
|
|
|
not contradiction |
(build in Mizar system) |
|
A & not contradiction |
[A and TRUE] |
|
| 1 |
8.1 |
|
|
|
|
|
|
|
|
|
TRUE |
(margrel:def 14) |
|
TRUE = 1 |
[TRUE is equal to 1.] |
|
| 1 |
8.2 |
T |
|
|
|
|
|
|
|
\top |
TRUE |
(margrel:def 14) |
|
TRUE = 1 |
[TRUE is equal to 1.] |
|
| 1 |
9 |
F |
f |
falsum |
FALSE |
0 |
falsity, falsum |
|
|
|
contradiction |
(build in Mizar system) |
|
A implies contradiction |
[A implies FALSE] |
|
| 1 |
9.1 |
|
|
|
|
|
|
|
|
|
FALSE |
(margrel:def 13) |
|
FALSE = 0 |
[FALSE is equal to 0.] |
|
| 1 |
9.2 |
⊥ |
|
|
|
|
|
|
|
\bot |
FALSE |
(margrel:def 13) |
|
FALSE = 0 |
[FALSE is equal to 0.] |
|
| 1 |
10 |
∴ |
|
|
|
|
|
結論 |
文頭に記され、その文の主張が前述の内容を受けて述べられていることを示す。 |
\therefore |
|
|
|
|
|
|
| 1 |
11 |
∵ |
|
|
|
|
|
理由・根拠 |
文頭に記され、その文の内容が前述の内容の理由説明であることを示す。それゆえ。 |
\because |
then |
|
|
A; then B; |
|
|
| 1 |
12 |
:= |
:⇔ |
|
|
|
|
定義 |
「A := X」は、A という記号の意味するところを、X と定義することである。「A :⇔ X」とも書く。 |
|
|
|
|
|
|
|
| 1 |
13 |
|
|
|
|
|
|
|
よって、それ故に、故に |
|
then |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 2 |
0 |
＜The notations of set theory＞ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 2 |
0.1 |
P(x)} |
|
|
|
|
|
|
S の元のうち、命題 P(x) が真であるもの全てを集めた集合。必要がなければ「∈ S」は省略する。 |
|
|
|
|
|
|
|
| 2 |
1 |
∈ |
|
|
|
|
element (of set) |
集合に属すること |
「x ∈ S」は、x が集合 S の元であることを意味する。必要に応じて「S ∋ x」とも書くが、こちらには S が主語であるようなニュアンスを伴うこともある。 |
\in |
in |
(hidden:pred 1) |
|
a in b |
[a is an element of b: a belongs to b.] |
|
| 2 |
1.1 |
∋ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 2 |
1.2 |
|
|
|
|
|
|
∈ の否定 |
「￢(x ∈ S)」を「x ? S」と書く。 |
\not\in |
|
|
|
|
|
|
| 2 |
1.3 |
? |
|
|
|
|
|
∋ の否定 |
「￢(S ∋ x)」を「S ? x」と書く。 |
\not\ni |
|
|
|
|
|
|
| 2 |
2 |
= |
|
|
|
|
equality (of set) |
集合の一致 |
「S = T」は集合 S と集合 T が等しいことを示す。 |
= |
= |
(hidden:pred 2) |
|
a = b |
[a is equal to b.] |
|
| 2 |
3 |
≠ |
|
|
|
|
the negation of equality (of set) |
=の否定 |
|
\neq |
<> |
(hidden:prednot 2) |
|
a <> b |
[a is not equal to b.] |
|
| 2 |
4 |
{ , } |
|
|
|
|
finite set with elements |
|
|
|
{ , } |
(tarski :def 1, etc.) |
1 |
{a} |
[set with an element a.] |
|
| 2 |
4.1 |
|
|
|
|
|
|
|
|
|
|
|
2 |
{a, b} |
[set with elements a, b] |
|
| 2 |
5 |
⊆ |
|
|
|
|
relation of inclusion (of set) |
部分集合 |
「S ⊆ T」は S が T の部分集合であることを意味する。必要に応じて「T ⊇ S」とも書く。他も同じ。 |
\subseteqq |
c= |
(tarski:def 3) |
|
a c= b |
[a is included in b: b includes a: a is a subset of b.] |
|
| 2 |
5.1 |
⊇ |
|
|
|
|
|
|
|
\supseteqq |
|
|
|
|
|
|
| 2 |
5.2 |
? |
|
|
|
|
|
|
|
\varsubsetneqq |
|
|
|
|
|
|
| 2 |
5.3 |
? |
|
|
|
|
|
|
|
\varsupsetneqq |
|
|
|
|
|
|
| 2 |
6 |
∪ |
|
|
|
|
union (of set) |
|
和集合 |
\bigcup |
union |
(tarski:def 3) |
|
union a |
[the union of a] |
|
| 2 |
7 |
∩ |
|
|
|
|
intersection (of set) |
|
積集合 |
\bigcap |
meet |
(setfam_1:def 1) |
|
meet a |
[the meet of a] |
|
| 2 |
8 |
[ , ] |
|
|
|
|
ordered pair |
|
|
|
[ , ] |
(tarski:def 5) |
|
[a, b] |
[the ordered pair of a and b] |
|
| 2 |
9 |
? |
|
|
|
|
empty set |
|
|
\emptyset |
{ } |
(xbool_0:def 1) |
|
{ } |
[{ } has no element.] |
|
| 2 |
10 |
∪ |
|
|
|
|
union (of two sets) |
|
|
\cup |
\/ |
(xbool_0:def 2) |
|
a \/ b |
[the union of a and b] |
|
| 2 |
11 |
∩ |
|
|
|
|
intersection (of two sets) |
|
|
\cap |
/\ |
(xbool_0:def 3) |
|
a /\ b |
[the intersection of a and b] |
|
| 2 |
12 |
＼ |
|
|
|
|
difference (of two sets) |
|
|
|
\ |
(xbool_0:def 4) |
|
a \ b |
[the set { x : x is an element of a and x is not an element of b}] |
|
| 2 |
13 |
⊂ |
|
|
|
|
relation of proper subset( of set) |
真部分集合 |
⊂ は真部分集合の場合のみを表す。 ただし、⊂ に「等しい場合」を含む流儀もあり、その場合、真部分集合であることを示すには \subsetneq を用いる。 |
\subset |
c< |
(xbool_0:def 8) |
|
a c< b |
[a is a proper subset of b] |
|
| 2 |
13.1 |
⊃ |
|
|
|
|
|
|
|
\supset |
|
|
|
|
|
|
| 2 |
14 |
|
|
|
|
|
complement (of set) |
|
補集合 |
(a)^c |
` |
(subset_1:def 5) |
|
a ` |
[the complement of a] |
|
| 2 |
14.1 |
￣ |
|
|
|
|
complement (of set) |
|
補集合 |
\bar{a} |
` |
(subset_1:def 5) |
|
a ` |
[the complement of a] |
|
| 2 |
15 |
× |
|
|
|
|
direct product of (sets) |
|
|
|
[:,:] |
(zfmisc_1:defs 3) |
1 |
[:a, b:] |
[the direct product of a and b] |
|
| 2 |
15.1 |
|
|
|
|
|
|
|
|
|
|
|
2 |
[:a, b, c:] |
[the direct product of a, b and c] |
|
| 2 |
16 |
P ( ) |
|
|
|
|
power set (of set) |
|
|
|
bool |
(zfmisc_1:def 1) |
|
bool a |
[the power set of a] |
|
| 2 |
17 |
{ x : P } |
|
|
|
|
the set of elements x such that P holds ) |
|
|
\{ x:P\} |
{ x : P } |
(build in Mizar system) |
1 |
{ x : P } |
[the set of elements x such that P holds] |
|
| 2 |
17.1 |
|
|
|
|
|
|
|
|
|
|
|
2 |
{ x where P : Q} |
[the set of element x satisfied with P such that Q holds] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 3 |
0 |
＜The notations of the sets of numbers＞ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 3 |
1 |
N |
|
|
|
|
the set of natural numbers with 0 |
|
{0,1,2,3,…,∞} |
\mathbb{N} |
NAT |
(numbers:funcnod 1) |
|
0 in NAT |
[0 is an element of N.] |
|
| 3 |
2 |
ω |
|
|
|
|
the least set of limit ordinals |
|
{0,1,2,3,…,∞}、NAT：自然数と同じ |
\mathbb{\omega} |
omega |
(ordinal2:def 5) |
|
0 in omega |
[0 is an element of ω.] |
|
| 3 |
3 |
Z |
|
|
|
|
the set of integers |
|
{-∞,…,-2,-1,0,1,2,…,∞} |
\mathbb{Z} |
INT |
(numbers:def 4) |
|
NAT c= INT |
[N is a subset of Z.] |
|
| 3 |
4 |
Q |
|
|
|
|
the set of rational numbers |
|
|
\mathbb{Q} |
RAT |
(numbers:def 3) |
|
NAT c= RAT |
[N is a subset of Q.] |
|
| 3 |
5 |
R |
|
|
|
|
the set of real numbers |
|
|
\mathbb{R} |
REAL |
(numbers:def 1) |
|
RAT c= REAL |
[Q is a subset of R.] |
|
| 3 |
6 |
C |
|
|
|
|
the set of complex numbers |
|
|
\mathbb{C} |
COMPLEX |
(numbers:def 2) |
|
REAL c= COMPLEX |
[R is a subset of C.] |
|
| 3 |
7 |
On |
|
|
|
|
the set of ordinals |
|
|
\mathbb{On} |
On |
(ordinal2:def 2) |
|
omega c= On |
[ω is a subset of On.] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 4 |
0 |
＜The notations for functions (relations)＞ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 4 |
1 |
dom |
|
|
|
|
domain (of function (relation)) |
|
定義域 |
|
dom |
(relat_1:def 4) |
|
dom f |
[dom f is the domain of f.] |
|
| 4 |
2 |
im |
|
|
|
|
(rng) range (of function (relation)) |
|
値域 |
|
rng |
(relat_1:def 5) |
|
rng f |
[rng f is the range of f.] |
|
| 4 |
3 |
|
|
|
|
|
inverse (of relation) |
|
逆数 |
\left( r \right)^{-1} |
~ |
(relat_1:def 7) |
|
r ~ |
[r ~ is the inverse relation of r.] |
|
| 4 |
4 |
|
|
|
|
|
inverse (of function) |
|
逆関数 |
\left( f \right)^{-1} |
“ |
(relat_1:def 14) |
|
f “ |
[f “ is the inverse relation of f.] |
|
| 4 |
5 |
? |
|
|
|
|
composition (of function (relation)) |
|
関数どうしの演算 |
\circ |
* |
(relat_1:def 8) |
|
f * g |
[f * g is the composition of f and g.] |
|
| 4 |
6 |
1/f |
|
|
|
|
the reciprocal of function f |
|
|
|
^ |
(rfunct_1:def 8) |
|
f ^ |
[f ^ is the reciprocal of function f , that is, for every x, (f^)(x)=1/(f.x).] |
|
| 4 |
7 |
a・f |
af |
|
|
|
scalar product of a scalar a and a real function f |
|
|
|
a (#) f |
(seq_1:def 5) |
|
(a (#) f) .b = a * (f.b) |
[ (af)(b) = a(f(b) ) ] |
|
| 4 |
7.1 |
|
|
|
|
|
|
|
|
|
a “ f |
(seq_1:def 5) |
|
(a “ f) .b = a * (f.b) |
[ (af)(b) = a(f(b) ) ] |
|
| 4 |
8 |
+ |
|
|
|
|
addition of functions |
|
|
+ |
+ |
(seq_1:def 3) |
|
f + g |
[f + g is addition of functions, that is , for every x, (f + g)(x) = f(x) +g(x).] |
|
| 4 |
9 |
－ |
|
|
|
|
subtraction of functions |
|
|
- |
- |
(seq_1:def 4) |
|
f - g |
[f - g is subtraction of functions, that is , for every x, (f - g)(x) = f(x) - g(x).] |
|
| 4 |
10 |
・ |
|
|
|
|
multiplication of functions |
|
|
\cdot |
(#) |
(seq_1:def 1) |
|
f (#) g |
[f (#)g is product of functions, that is , for every x, (f (#) g )(x) = f(x)・g(x).] |
|
| 4 |
11 |
f/g |
|
|
|
|
fraction of functions |
|
|
|
/ |
(rfunct_1:def 4) |
|
f/g |
[f/g is fraction of functions, that is , for every x, (f/g)(x)=(f(x)/g(x)).] |
|
| 4 |
12 |
－ |
|
|
|
|
the inverse of function with respect to addition |
|
|
|
- |
(seq_1:def 7) |
|
- f |
[-f is inverse of function with respect to addition, that is , for every x, (-f )(x) = -f(x) .] |
|
| 4 |
13 |
｜ |
|
|
|
|
restriction (of function (relation)) |
|
|
\mid |
｜ |
(relat_1:def 11) |
|
f｜a |
a? is the restriction of f with respect to a.] |
|
| 4 |
14 |
f (a) |
|
|
|
|
image of a value a (with respect to function (relation) f ) |
|
|
|
f.a |
(funct_1:def 4) |
|
f.a |
[f.a is the image of a with respect to f.] |
|
| 4 |
14.1 |
|
|
|
|
|
image of natural number i of values |
|
|
\a_i |
a.i |
(funct_1:def 4) |
|
a.i |
|
|
| 4 |
15 |
f (A) |
|
|
|
|
image of set A of values (with respect to function (relation) f ) |
|
|
|
f .: A |
(relat_1:def 13) |
|
f.:A |
[f.:A is the image of set A of values with respect to f.] |
|
| 4 |
16 |
Hom(X, Y) |
|
|
|
|
the set of functions with domain X and range Y |
|
|
|
Funcs( , ) |
(funct_2:def 2) |
|
f in Funcs(X, Y) implies rng f = Y |
[(f is an element of Hom(X, Y)) implies rng f = Y.] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 5 |
0 |
＜The notations of arithmetic＞ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 5 |
1 |
+ |
|
|
|
|
addition |
|
|
+ |
+ |
(xcmplx_0:def 4) |
|
a + b |
[a + b is the sum of a and b.] |
|
| 5 |
2 |
・ |
|
|
|
|
multiplication |
|
|
\cdot |
* |
(xcmplx_0:def 5) |
|
a * b |
[a * b is the product of a and b.] |
|
| 5 |
2.1 |
× |
|
|
|
|
multiplication |
|
|
\times |
* |
|
|
|
|
|
| 5 |
3 |
－ |
|
|
|
|
subtraction |
|
|
- |
- |
(xcmplx_0:def 8) |
|
a - b |
[a - b is the difference of a and b.] |
|
| 5 |
4 |
－ |
|
|
|
|
negative sign (minus sign) |
|
|
- |
- |
(xcmplx_0:def 6) |
|
-a |
[-a is a negative number.] |
|
| 5 |
5 |
/ |
|
|
|
|
fraction |
分数 |
|
\frac{b}{a} |
/ |
(xcmplx_0:def 9) |
|
a / b |
[a / b is a fraction with numerator a and denominator b.] |
|
| 5 |
6 |
1/a |
|
|
|
|
the reciprocal (number) of a |
逆数 |
|
1/a |
“ |
(xcmplx_0:def 7) |
|
a“ |
[a“ is the reciprocal (number) of a, that is 1/a.] |
|
| 5 |
7 |
÷ |
|
|
|
|
division |
|
|
\div |
div |
(int_1:def 7) |
|
a div b |
[a div b is the quotient when b devides a.] |
|
| 5 |
8 |
mod |
|
|
|
|
residue |
|
|
|
mod |
(int_1:def 8) |
|
a mod b |
[a mod b is the remainder when b devides a.] |
|
| 5 |
9 |
｜ |
|
|
|
|
devides |
|
|
\mid |
devides |
(int_1:def 9) |
|
a｜b |
b means that a devides b.] |
|
| 5 |
10 |
lcm |
|
|
|
|
the least common multiple (of two natural numbers) |
|
|
|
lcm |
(nat_1:def 4 |
|
a lcm b |
[a lcm b is the least common multiple of a and b.] |
|
| 5 |
11 |
lcm |
|
|
|
|
the least common multiple (of two integers) |
|
|
|
lcm’ |
(int_2:def 2 |
|
a lcm’ b |
a| and |b|.] |
|
| 5 |
12 |
gcd |
|
|
|
|
the greatest common divisor of two natural numbers) |
|
|
\gcd |
hcf |
(nat_1:def 5) |
|
a hcf b |
[a gcd b is the greatest common divisorof a and b.] |
|
| 5 |
13 |
gcd |
|
|
|
|
the greatest common divisor (of two integers) |
|
|
\gcd |
gcd |
(nat_1:def 5) |
|
a gcd b |
a| and |b|.] |
|
| 5 |
14 |
‘ |
|
|
|
|
successor function |
|
|
|
succ |
(ordinal1:def 1) |
|
succ a |
[succ a is the successor of a] |
|
| 5 |
15 |
≦ |
|
|
|
|
inequality with equality |
|
|
\leqq |
<= |
(xreal_0:def 2) |
|
1 <= 2 |
[1 is smaller than 2.] |
|
| 5 |
16 |
＞ |
|
|
|
|
inequality |
|
|
> |
> |
(xreal_0:prednot 4) |
|
2 > 1 |
[2 is larger than 1.] |
|
| 5 |
17 |
≧ |
|
|
|
|
inequality with equality |
|
|
\geqq |
=> |
(xreal_0:prednot 2) |
|
2 => 1 |
[2 is larger than 1.] |
|
| 5 |
18 |
＜ |
|
|
|
|
inequality |
|
|
< |
< |
(xreal_0:prednot 2) |
|
1 < 2 |
[1 is smaller than 2.] |
|
| 5 |
19 |
min |
|
|
|
|
minimum |
最小値 |
|
\min |
min |
(extreal2:def 1) |
|
min(2,3) = 2 |
[2 is minimum with respect to 2 and 3.] |
|
| 5 |
20 |
max |
|
|
|
|
maximum |
最大値 |
|
\max |
max |
(extreal2:def 2) |
|
max(2,3) = 3 |
[3 is maximum with respect to 2 and 3.] |
|
| 5 |
21 |
! |
|
|
|
|
factorial (of a natural number) |
階乗 |
|
! |
! |
(sin_cos:def 30) |
|
a ! |
[a ! is the factorial of a natural number a] |
|
| 5 |
22 |
[ ] |
|
|
|
|
Gauss'symbol |
|
|
[a] |
[\ /] |
(int_1:def 4) |
|
[\a/] |
[[\ a/] is [a].」 |
|
| 5 |
23 |
a≡b(mod c) |
|
|
|
|
a and b are congruent modulo c |
|
|
\equiv |
, are_congruent_mod |
(int_1:def 3) |
|
a , b are_congruent_mod c |
[(a , b are_congruent_mod c) means (a ≡ b (mod c) )] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 6 |
0 |
＜The notations of numbers and special constants＞ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 6 |
1 |
0 |
|
|
|
|
numeral zero |
|
|
0 |
0 |
|
|
|
|
|
| 6 |
2 |
1 |
|
|
|
|
numeral one |
|
|
1 |
1 |
|
|
|
|
|
| 6 |
2.1 |
1 |
|
|
|
|
numeral one |
|
|
1 |
one |
(ordinal2:def 2) |
|
|
|
|
| 6 |
3 |
2 |
|
|
|
|
numeral two |
|
|
2 |
2 |
|
|
|
|
|
| 6 |
4 |
3 |
|
|
|
|
numeral three |
|
|
3 |
3 |
|
|
|
|
|
| 6 |
5 |
4 |
|
|
|
|
numeral four |
|
|
4 |
4 |
|
|
|
|
|
| 6 |
6 |
5 |
|
|
|
|
numeral five |
|
|
5 |
5 |
|
|
|
|
|
| 6 |
7 |
6 |
|
|
|
|
numeral six |
|
|
6 |
6 |
|
|
|
|
|
| 6 |
8 |
7 |
|
|
|
|
numeral seven |
|
|
7 |
7 |
|
|
|
|
|
| 6 |
9 |
8 |
|
|
|
|
numeral eight |
|
|
8 |
8 |
|
|
|
|
|
| 6 |
10 |
9 |
|
|
|
|
numeral nine |
|
|
9 |
9 |
|
|
|
|
|
| 6 |
11 |
π |
|
|
|
|
circle ratio |
|
|
\pi |
PI |
(sin_cos:def 30) |
|
3 < PI |
[πis greater than 3.] |
|
| 6 |
12 |
e |
|
|
|
|
Napier’s number |
|
|
|
number_e |
(power:def 4) |
|
2 < number_e |
[e is greater than 2.] |
|
| 6 |
13 |
i |
|
|
|
|
imaginary number |
|
|
|
|
(xcmplx_0:def 1) |
|
|
|
|
| 6 |
14 |
∞ |
|
|
|
|
infinity |
|
|
\infty |
+infty |
(supinf_1:def 1) |
|
|
|
|
| 6 |
14.1 |
-∞ |
|
|
|
|
infinity |
|
|
?\infty |
?infty |
(supinf_1:def 3) |
|
|
|
|
| 6 |
15 |
+∞ |
|
|
|
|
infinity |
|
|
+\infty |
+infty |
(supinf_1:def 1) |
|
|
|
|
| 6 |
16 |
-∞ |
|
|
|
|
infinity |
|
|
?\infty |
?infty |
(supinf_1:def 3) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 7 |
0 |
＜The notations for elementary functions and complex numbers＞ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 7 |
1 |
sin |
|
|
|
|
sin |
|
|
\sin |
sin |
(sin_cos:def 30) |
|
sin a |
[the sine of a.] |
|
| 7 |
2 |
cos |
|
|
|
|
cos |
|
|
\cos |
cos |
(sin_cos:def 22) |
|
cos a |
[the cosine of a.] |
|
| 7 |
3 |
tan |
|
|
|
|
tan |
|
|
\tan |
tan |
(sin_cos4:def 1) |
|
tan a |
[the tangent of a.] |
|
| 7 |
4 |
sec |
|
|
|
|
sec |
|
|
\sec |
sec |
(sin_cos4:def 4) |
|
sec a |
[the second of a.] |
|
| 7 |
5 |
cot |
|
|
|
|
cot |
|
|
\cot |
cot |
(sin_cos4:def 2) |
|
cot a |
[the cotangent of a.] |
|
| 7 |
6 |
arcsin |
|
|
|
|
arcsin |
|
|
\arcsin |
arcsin |
(sin_cos6:def 1) |
|
arcsin a |
[the arcsine of a.] |
|
| 7 |
7 |
arccos |
|
|
|
|
arccos |
|
|
\arccos |
arccos |
(sin_cos6:def 3) |
|
arccos a |
[the arccosine of a.] |
|
| 7 |
8 |
|
|
|
|
|
exponential function (of real values) |
|
|
\exp |
exp |
(sin_cos:def 26) |
|
exp x |
[the exponential function of x] |
|
| 7 |
9 |
Re |
|
|
|
|
the real part of a complex number |
|
|
|
Re |
(complex1:dfs 1) |
|
Re a |
[the real part of a complex number a] |
|
| 7 |
10 |
Im |
|
|
|
|
the imaginary part of a complex number |
|
|
|
Im |
(complex1:dfs 2) |
|
Im a |
[the imaginary part of a complex number a] |
|
| 7 |
11 |
√ |
|
|
|
|
positive square root (of a real number) |
|
|
\sqrt{} |
sqrt |
(square_1:def 4) |
|
sqrt a |
[the square root of a] |
|
| 7 |
12 |
|
|
|
|
|
positive n-powered root (of a real number) |
|
|
\sqrt[n]{} |
n-Root |
(prepower:def 3) |
|
3 -Root a |
[the positive cubic root of a] |
|
| 7 |
13 |
|
|
|
|
|
squre (of a number) |
|
|
^2 |
^2 |
(square_1:def 3) |
|
a^2 |
[the square of a] |
|
| 7 |
13.1 |
|
|
|
|
|
squre (of a number) |
|
|
^2 |
sqr |
(square_1:def 3) |
|
a^2 |
[the square of a] |
|
| 7 |
14 |
|
|
|
|
|
a real number with exponent of a natural number |
|
|
a^b |
^ |
(newton:def 1) |
|
^ b |
[the b times power of real number a] |
|
| 7 |
14.1 |
|
|
|
|
|
a real number with exponent of an integer |
|
|
a^b |
#Z |
(prepower:def 4) |
|
a #Z b |
[the b times power of real number a] |
|
| 7 |
14.2 |
|
|
|
|
|
a real number with exponent of a rational namber |
|
|
a^b |
#Q |
(prepower:def 5) |
|
a #Q b |
[the b power of real number a] |
|
| 7 |
14.3 |
|
|
|
|
|
a real number with exponent of a real number |
|
|
a^b |
#R |
(prepower:def 8) |
|
a #R b |
[the b power of real number a] |
|
| 7 |
14.4 |
|
|
|
|
|
a real number with exponent of a real number |
|
|
a^b |
to_power |
(power:def 2) |
|
a to_power b |
[the b power of real number a] |
|
| 7 |
15 |
｜｜ |
|
|
|
|
absolute value (of a complex number) |
|
|
\mid a \mid |
abs |
(complex1:func 18) |
|
abs a |
[the absolute value of a] |
|
| 7 |
16 |
￣ |
|
|
|
|
conjugate complex number (of complex number) |
|
|
|
*’ |
(complex1:def 15) |
|
*’ |
[*’ = －] |
|
| 7 |
17 |
log |
|
|
|
|
logarithm |
|
|
\log |
log( , ) |
(power:def 3) |
|
log(a,b) |
[log(a,b) is a logarithm with base of logarithm a and anti-logarithm b.] |
|
| 7 |
18 |
a + bi |
|
|
|
|
a complex number with its real part a and its imaginary part b ), where a and b are real numbers |
|
|
|
[*a,b*] |
(arytm_0:def 7) |
|
for a being Element of REAL holds [*a,0*] in REAL |
[It means that for a∈R，a+0i∈R holds.] |
|
| 7 |
19 |
arg |
|
|
|
|
the argument of a complex number |
|
|
|
Arg |
(comptrig:def 1) |
|
Arg a |
[Arg a is the argument of a complex number a.] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 8 |
0 |
＜The notations for limit and series＞ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 8 |
1 |
lim |
|
|
|
|
limit of complex sequence |
|
|
\lim |
lim |
(comseq_2:def 5) |
1 |
lim a |
[the limit of complex sequence a] |
|
| 8 |
1.1 |
|
|
|
|
|
|
|
|
|
|
|
2 |
lim (a+b) = lim a + lim b |
[This holds if a and b are convergent.] |
|
| 8 |
2 |
∑ |
|
|
|
|
pertial sum of a real sequence |
|
|
\sum |
Percial_Sums |
(series_1:def 1) |
|
Percial_Sums a |
[pertial sum of real sequence a] |
|
| 8 |
3 |
∑ |
|
|
|
|
sum of infinite series |
|
|
\sum |
Sum |
(series_1:def 3) |
1 |
Sums a |
[sum of infinite series of a real sequence a] |
|
| 8 |
3.1 |
|
|
|
|
|
|
|
|
|
|
|
2 |
Sums a = lim Percial_Sums a |
[The sum of infinite series of a real sequence a is equal to the limit of the pertial sum of it.] |
|
| 8 |
4 |
→+∞ |
|
|
|
|
(for a real sequence) divergent to the plus infinity |
|
|
|
(is) divergent_to+infty |
(limfunc1:def 4) |
|
a is divergent_to+infty |
[The real sequence a is divergent to the plus infinity, that is , a →+∞.] |
|
| 8 |
5 |
→－∞ |
|
|
|
|
(for a real sequence) divergent to the minus infinity |
|
|
|
(is) divergent_to-infty |
(limfunc1:def 5) |
|
a is divergent_to-infty |
[The real sequence a is divergent to the minus infinity, that is , a →－∞.] |
|
| 8 |
6 |
|
|
|
|
|
limit b of a real function（x → a ） |
|
|
\lim_{x \to a} f(x) = b |
lim( , ) |
(limfunc3: def 4) |
|
lim(f ,a) = b |
[f is convergent to b in a.] |
|
| 8 |
7 |
|
|
|
|
|
limit b of a real function（x → a + 0 ） |
|
|
\lim_{x \to a+0 } f(x)= b |
lim_right( , ) |
(limfunc2: def 8) |
|
lim_right(f ,a) = b |
[f is right-convergent to b in a.] |
|
| 8 |
8 |
|
|
|
|
|
limit b of a real function（x → a － 0 ） |
|
|
\lim_{x \to a-0 } f(x)= b |
lim_left( , ) |
(limfunc2: def 7) |
|
lim_left(f ,a) = b |
[f is left-convergent to b in a.] |
|
| 8 |
9 |
|
|
|
|
|
a real function f is divergent to +∞（x → a） |
|
|
\lim_{x \to a } f(x)= +\infty |
is_divergent_to+infty_in |
(limfunc3: def 2) |
|
f is_divergent_to+infty_in a |
[f is divergent to +∞ in a.] |
|
| 8 |
10 |
|
|
|
|
|
a real function f is divergent to －∞（x → a） |
|
|
\lim_{x \to a } f(x)= -\infty |
is_divergent_to-infty_in |
(limfunc3: def 3) |
|
f is_divergent_to-infty_in a |
[f is divergent to －∞ in a.] |
|
| 8 |
11 |
|
|
|
|
|
a real function f is divergent to +∞（x → a + 0 ） |
|
|
\lim_{x \to a+0 } f(x)= +\infty |
is_right_divergent_to+infty_in |
(limfunc2:def 5) |
|
f is_ right_divergent_to+infty_in a |
[f is right-divergent to +∞ in a.] |
|
| 8 |
12 |
|
|
|
|
|
a real function f is divergent to －∞（x → a + 0 ） |
|
|
\lim_{x \to a+0 } f(x)= -\infty |
is_right_divergent_to-infty_in |
(limfunc2:def 6) |
|
f is_ right_divergent_to-infty_in a |
[f is right-divergent to －∞ in a.] |
|
| 8 |
13 |
|
|
|
|
|
a real function f is divergent to +∞（x → a － 0 ） |
|
|
\lim_{x \to a-0 } f(x)= +\infty |
is_left_divergent_to+infty_in |
(limfunc2:def 2) |
|
f is_ left_divergent_to+infty_in a |
[f is left-divergent to +∞ in a.] |
|
| 8 |
14 |
|
|
|
|
|
a real function f is divergent to －∞（x → a － 0 ） |
|
|
\lim_{x \to a-0 } f(x)= -\infty |
is_left_divergent_to-infty_in |
(limfunc2:def 3) |
|
f is_ left_divergent_to-infty_in a |
[f is left-divergent to －∞ in a.] |
|
| 8 |
15 |
|
|
|
|
|
limit of a real function（x → +∞ ） |
|
|
\lim_{x \to +\infty } f(x)= a |
lim_in+infty |
(limfunc1:def 12) |
|
lim_in+infty f = a |
[the limit a of a real function f in the plus infinity] |
|
| 8 |
16 |
|
|
|
|
|
limit of a real function（x → －∞ ） |
|
|
\lim_{x \to -\infty } f(x)= a |
lim_in-infty |
(limfunc1:def 13) |
|
lim_in-infty f = a |
[the limit a of a real function f in the minus infinity] |
|
| 8 |
17 |
|
|
|
|
|
(for a real function) divergent to the plus infinity (x →+∞) |
|
|
\lim_{x \to +\infty } f(x)= +\infty |
(is) divergent_in+infty_to-infty |
(limfunc1:def 7) |
|
f is divergent_in+infty_to-infty |
[The real function f is divergent to the plus infinity when x →+∞.] |
|
| 8 |
18 |
|
|
|
|
|
(for a real function) divergent to the minus infinity (x →+∞) |
|
|
\lim_{x \to +\infty } f(x)= -\infty |
(is) divergent_in+infty_to-infty |
(limfunc1:def 8) |
|
f is divergent_in+infty_to-infty |
[The real function f is divergent to the minus infinity when x →+∞.] |
|
| 8 |
19 |
|
|
|
|
|
(for a real function) divergent to the plus infinity (x →－∞) |
|
|
\lim_{x \to -\infty } f(x)= +\infty |
(is) divergent_in-infty_to+infty |
(limfunc1:def 10) |
|
f is divergent_in-infty_to+infty |
[The real function f is divergent to the plus infinity when x →－∞.] |
|
| 8 |
20 |
|
|
|
|
|
(for a real function) divergent to the minus infinity (x →－∞) |
|
|
\lim_{x \to -\infty } f(x)= -\infty |
(is) divergent_in-infty_to-infty |
(limfunc1:def 11) |
|
f is divergent_in-infty_to-infty |
[The real function f is divergent to the minus infinity when x →－∞.] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 9 |
0 |
＜The notations for differentiation and integral＞ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 9 |
1 |
( , ) |
|
|
|
|
open interval |
|
|
|
]. , .[ |
(rcomp_1:def 2) |
|
].0 , 1.[ |
[This is the open interval between 0 and 1.] |
|
| 9 |
2 |
] , [ |
|
|
|
|
open interval |
|
|
|
]. , .[ |
(rcomp_1:def 2) |
|
].0 , 1.[ |
[This is the open interval between 0 and 1.] |
|
| 9 |
3 |
f’(a) |
|
|
|
|
differential coefficient of real function f in a |
|
|
|
diff(f, a) |
(fdiff_1:def 6) |
|
diff(f + g, a) = diff(f, a) + diff(g, a) |
[This means (f + g)’(a) = f’(a) + g’(a)] |
|
| 9 |
4 |
f ‘ (x) (x∈a) |
|
|
|
|
the differential of a real function f differentiable on a ⊆ R |
|
|
|
f `｜a |
(fdiff_1:def 8) |
|
f `｜REAL |
[This is the differential of the real function f differentiable on R.] |
|
| 9 |
5 |
f ‘ |
|
|
|
|
the differential of a real function f differentiable on R |
|
|
|
f `｜REAL |
(fdiff_1:def 8) |
|
(f `｜REAL).a |
[This is the differential coefficient of the real function f in a .] |
|
| 9 |
6 |
∫f(x)dx |
|
|
|
|
indefinite Riemann integral of a real function |
|
|
\int f(x) dx |
integral |
[integra1:def 18] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 10 |
0 |
＜The notations for geometry＞ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 10 |
1 |
AB |
|
|
|
|
line through A and B in 3 dimentional Euclidian space |
|
|
|
Line( , ) |
(euclid_1:def 1) |
1 |
Line(A,B) st A, B in REAL 3 |
[line through A and B in 3 dimentional Euclidian space, where A, B are real 3-tuples.] |
|
| 10 |
1.1 |
|
|
|
|
|
|
|
|
|
|
|
2 |
for A, B st A, B in REAL 3 holds Line(A,B) = Line(B,A) |
[line through A and B is equal to line through B and A.] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 11 |
0 |
＜The notations for probability＞ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 11 |
1 |
Pr |
|
|
|
|
probability |
|
|
|
Probability (of ) |
(prob_1:def 13) |
|
Probability of X |
[This means Pr(X), that is, the probability of an event X.] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 12 |
0 |
＜The notations for vectors and matrices＞ |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| 12 |
1 |
|
|
|
|
|
A is an n×m matrix over R |
|
|
A_{n m} |
A is Matrix of n,m,REAL |
(matrix_1: def 3) |
|
|
|
|
| 12 |
2 |
|
|
|
|
|
A is an n×m matrix over C |
|
|
A_{n m} |
A is Matrix of n,m,COMPLEX |
(matrix_1: def 3) |
|
|
|
|
| 12 |
3 |
|
|
|
|
|
1×…matrix a (line vector) |
|
|
(\vec{a}) |
<*a*> |
(matrix_1:11) |
|
|
|
|
| 12 |
4 |
|
|
|
|
|
1×ｎmatrix a (line vector) |
|
|
(\vec{a}) |
<*a*> st width <*a*> = n |
(matrix_1:11;matrix_1: def 4) |
|
|
|
|
| 12 |
4 |
|
|
|
|
|
…×1 matrix a (column vector) |
|
|
(\vec{a})^t |
<*a*>@? |
(matrix_1:11; matrix_1: def 7 ) |
|
|
|
|
| 12 |
5 |
|
|
|
|
|
n×1 matrix a (column vector) |
|
|
(\vec{a})^t |
<*a*>@ st width <*a*> = n |
(matrix_1:11; matrix_1: def 7 ) |
|
|
|
|
| 12 |
6 |
|
|
|
|
|
2×…matrix |
|
|
\begin{pmatrix} \vec{a} \\ \vec{b} \end{pmatrix} |
<*a,b*> |
(matrix_1:12) |
|
|
|
|
| 12 |
7 |
|
|
|
|
|
2×n matrix |
|
|
\begin{pmatrix} \vec{a} \\ \vec{b} \end{pmatrix} |
<*a,b*> st width <*a,b*> = n |
(matrix_1:12; matrix_1: def 4) |
|
|
|
|
| 12 |
8 |
|
|
|
|
|
…×2 matrix |
|
|
\begin{pmatrix} \vec{a} \\ \vec{b} \end{pmatrix}^t |
<*a,b*>@ |
(matrix_1:12; matrix_1: def 7) |
|
|
|
|
| 12 |
9 |
|
|
|
|
|
ｎ×2 matrix |
|
|
\begin{pmatrix} \vec{a} \\ \vec{b} \end{pmatrix}^t |
<*a,b*>@ st width <*a*> = n |
(matrix_1:12; matrix_1: def 7) |
|
|
|
|
| 12 |
10 |
|
|
|
|
|
1×1 matrix with element a matrix |
|
|
(a) |
<*<*a*>*> |
(matrix_1:15) |
|
|
|
|
| 12 |
11 |
|
|
|
|
|
1×2 matrix with elements a and b |
|
|
\begin{pmatrix} a & b \end{pmatrix} |
<*<*a*>,<*b*>*> |
(matrix_1:15) |
|
|
|
|
| 12 |
12 |
|
|
|
|
|
2×2 matrix with elements a, b, c and d |
|
|
\begin{pmatrix} a & b \\ c & d \end{pmatrix} |
<*<*a,b*>,<*c,d*>*> |
(matrix_1:15) |
|
|
|
|
| 12 |
13 |
|
|
|
|
|
2×2 matrix with elements a, b, c and d |
|
|
\begin{pmatrix} a & b \\ c & d \end{pmatrix} |
(a,b)][(b,c) |
(matrix_2:def 2) |
|
|
|
|
| 12 |
14 |
|
|
|
|
|
(i, j)-element of a matrix a |
|
|
a_{i j} |
A*(i,j) |
(matrix_1:def 6) |
|
|
|
|
| 12 |
15 |
|
|
|
|
|
transposed matrix of A |
|
|
A^t |
@ |
(matrix_1:def 7) |
|
A@ |
[A@ is the transposed matrix of A.] |
|
| 12 |
16 |
+ |
|
|
|
|
addition of matrices |
|
|
+ |
+ |
(matrix_1:def 7) |
|
a + b |
[the sum of matrices a and b] |
|
| 12 |
17 |
－ |
|
|
|
|
minus sign of matrix matrices |
|
|
- |
- |
(matrix_1:def 13) |
|
-a |
[the inverse of a matrix a with resprect to addition] |
|
| 12 |
18 |
・ |
× |
nothing |
|
|
multiplication of matrices |
|
|
|
* |
(matrix_3:def 4) |
|
a * b |
[the product of matrices a and b] |
|
| 12 |
19 |
( , ) |
< , > |
|
|
|
the inner product of finite sequences recognized as vectors |
|
|
|
“*” |
(fvsum_1:def 10) |
|
a“*”b |
[the inner product of finite sequences a and b recognized as vectors] |
|
| 12 |
20 |
|
|
|
|
|
the n-th line of a matrix a |
|
|
|
Line(a,n) |
(matrix_1:def 8) |
|
|
|
|
| 12 |
21 |
|
|
|
|
|
the n-th colum of a matrix a |
|
|
|
Col(a,n) |
(matrix_1:def 9) |
|
|
|
|
| 12 |
22 |
O |
|
|
|
|
n×m zero matrix |
|
|
|
0.(n,m) |
(matrix_1:def 11) |
|
|
|
|
| 12 |
23 |
E |
I |
|
|
|
n×n unit matrix |
|
|
|
1.(n,m) |
(matrix_1:def 12) |
|
|
|
|
| 12 |
24 |
det a |
|
|
|
|
the determinant of a matrix a |
|
|
|
Det |
(matrix_1:def 12) |
|
Det a |
[the determinant of a matrix a] |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
{A} |
|
|
|
|
|
|
集合に属性を持たせる |
|
[#] |
() |
|
[#]A [topologyの属性] |
|
|
|
|
⊂ |
⊆ |
|
|
|
|
|
Aの部分集合 |
|
Subset of A |
|
|
Subset of A |
|
|
|
|
|
|
|
|
|
TopStruct (# carrier -> set,topology -> Subset-Family of the carrier #) |
|
TopStruct (# 領域,条件式 #) |
|
TopStruct(#X,T#) |
(PRE_TOPC:) |
|
TopStruct(#X,T#) |
|
|
|
|
|
|
|
|
|
|
|
Aの和集合 |
|
union A |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
順序集合 |
|
1-sorted |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Tの要素、範囲 |
|
the carrier of T |
|
|
the carrier of T |
|
|
|
|
|
|
|
|
|
|
|
Aの補集合 |
|
{}A |
|
|
|
|
|
|
|
{A} |
|
|
|
|
|
|
集合A |
|
[#]A |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
開集合X |
|
[#]X is open |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
閉集合X |
|
[#]X is closed |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
写像 |
|
Morphism |
|
|
|
|
|
|
|
|
|
|
|
|
relation |
|
関係 |
|
relation |
|
|
|
|
|
|
|
|
|
|
|
|
reflexive |
|
反射的 |
|
reflexive |
|
|
|
|
|
|
|
|
|
|
|
|
symmetric |
|
対称的 |
|
symmetric |
|
|
|
|
|
|
|
|
|
|
transitive |
|
推移的 |
|
transitive |
|
|
|
|
|
|
|
|
|
|
antisymmetric |
|
反対称的 |
|
antisymmetric |
|
|
|
|
|
|
|
|
|
|
|
|
一対一の対応 |
|
one-to-one |
|
|
|
|
|
|
|
|
|
|
Cardinality |
|
濃度 |
|
Cardinality |
|
|
|
|
|
|
|
|
|
|
cardinal Number |
|
基数 |
|
cardinal Number |
|
|
|
|
|
|
|
|
|
|
finite set |
|
有限集合 |
|
finite set |
|
|
|
|
|
(x0,x1,…,xn) |
|
|
|
|
n-tuple |
|
n組の直積集合 |
|
n-tuple |
|
|
|
|
|
|
|
|
|
|
Inverse mapping |
|
逆写像 |
|
Inverse mapping |
|
|
|
|
|
|
|
|
|
|
element |
|
要素、元 |
|
Element |
|
|
|
|
|
|
|
|
|
|
definition(定義) + predicate(述語) |
|
|
|
defpred |
|
|
|
|
|
|
|
|
|
|
述語(predicate) |
|
|
|
pred |
|
|
|
|
|
|
|
|
|
|
then + thus |
|
|
|
hence |
|
|
|
|
|
|
|
|
|
|
IDENTITY RELATION |
|
同値関係 |
|
id |
|
|
|
|
|
|
|
|
|
|
|
|
概念の包含関係をしめすときに使う |
|
cluster |
|
|
|
|
|
|
|
|
|
|
|
|
内包 |
|
Int |
TOPS_1 |
|
Int [#]A
|
|
|
∂A |
|
|
|
|
|
|
外包 |
|
boundary |
TOPS_1 |
|
A is boundary
|
|
|
X1-X2| |
|
|
|
|
|
|
X1,X2の距離 |
|
dist(X1,X2) |
JGRAPH_1 |
|
dist(X1,X2)
|
|
|
|
|
|
|
|
|
|
距離空間 |
|
MetrSpace |
|
|
|
|
|
|
|
|
|
|
|
|
関数の要素 |
|
PartFunc |
|
|
|
|
|
bi |
|
|
|
|
|
|
i番目の要素 |
|
b/.i |
BINARITH |
|
|