Mizar/記号

		数学記号					意味		説明	[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	$\notin$						∈ の否定	「￢(x ∈ S)」を「x ? S」と書く。	\not\in
2	1.3	?	$\not \ni$					∋ の否定	「￢(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$							\varsubsetneqq
2	5.3	?	$\varsupsetneqq$							\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	?	$\emptyset$				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	$()^{c}$					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	$\mathbb {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	ω	$\mathbb {\omega }$				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	$\mathbb {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	$\mathbb {Q}$				the set of rational numbers			\mathbb{Q}	RAT	(numbers:def 3)		NAT c= RAT	[N is a subset of Q.]
3	5	R	$\mathbb {R}$				the set of real numbers			\mathbb{R}	REAL	(numbers:def 1)		RAT c= REAL	[Q is a subset of R.]
3	6	C	$\mathbb {C}$				the set of complex numbers			\mathbb{C}	COMPLEX	(numbers:def 2)		REAL c= COMPLEX	[R is a subset of C.]
3	7	On	$\mathbb {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	$\left(r\right)^{-1}$					inverse (of relation)		逆数	\left( r \right)^{-1}	~	(relat_1:def 7)		r ~	[r ~ is the inverse relation of r.]
4	4	$\left(f\right)^{-1}$					inverse (of function)		逆関数	\left( f \right)^{-1}	“	(relat_1:def 14)		f “	[f “ is the inverse relation of f.]
4	5	?	$\circ$				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	$a_{i}$					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	$e^{x}$					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	${\sqrt[{n}]{}}$					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	$()^{2}$					squre (of a number)			^2	^2	(square_1:def 3)		a^2	[the square of a]
7	13.1	$()^{2}$					squre (of a number)			^2	sqr	(square_1:def 3)		a^2	[the square of a]
7	14	$a^{b}$					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^{b}$					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^{b}$					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^{b}$					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^{b}$					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	$\lim _{x\to a}f(x)=b$					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	$\lim _{x\to a+0}f(x)=b$					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	$\lim _{x\to a-0}f(x)=b$					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	$\lim _{x\to a}f(x)=+\infty$					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	$\lim _{x\to a}f(x)=-\infty$					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	$\lim _{x\to a+0}f(x)=+\infty$					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	$\lim _{x\to a+0}f(x)=-\infty$					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	$\lim _{x\to a-0}f(x)=+\infty$					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	$\lim _{x\to a-0}f(x)=-\infty$					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	$\lim _{x\to +\infty }f(x)=a$					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	$\lim _{x\to -\infty }f(x)=a$					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	$\lim _{x\to +\infty }f(x)=+\infty$					(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	$\lim _{x\to +\infty }f(x)=-\infty$					(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	$\lim _{x\to -\infty }f(x)=+\infty$					(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	$\lim _{x\to -\infty }f(x)=-\infty$					(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_{nm}$					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_{nm}$					A is an n×m matrix over C			A_{n m}	A is Matrix of n,m,COMPLEX	(matrix_1: def 3)
12	3	$({\vec {a}})$					1×…matrix a (line vector)			(\vec{a})	<*a*>	(matrix_1:11)
12	4	$({\vec {a}})$					1×ｎmatrix a (line vector)			(\vec{a})	<*a*> st width <*a*> = n	(matrix_1:11;matrix_1: def 4)
12	4	$({\vec {a}})^{t}$					…×1 matrix a (column vector)			(\vec{a})^t	<*a*>@?	(matrix_1:11; matrix_1: def 7 )
12	5	$({\vec {a}})^{t}$					n×1 matrix a (column vector)			(\vec{a})^t	<*a*>@ st width <*a*> = n	(matrix_1:11; matrix_1: def 7 )
12	6	${\begin{pmatrix}{\vec {a}}\\{\vec {b}}\end{pmatrix}}$					2×…matrix			\begin{pmatrix} \vec{a} \\ \vec{b} \end{pmatrix}	<*a,b*>	(matrix_1:12)
12	7	${\begin{pmatrix}{\vec {a}}\\{\vec {b}}\end{pmatrix}}$					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	${\begin{pmatrix}{\vec {a}}\\{\vec {b}}\end{pmatrix}}^{t}$					…×2 matrix			\begin{pmatrix} \vec{a} \\ \vec{b} \end{pmatrix}^t	<*a,b*>@	(matrix_1:12; matrix_1: def 7)
12	9	${\begin{pmatrix}{\vec {a}}\\{\vec {b}}\end{pmatrix}}^{t}$					ｎ×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	$(a)$					1×1 matrix with element a matrix			(a)	<*<*a*>*>	(matrix_1:15)
12	11	${\begin{pmatrix}a&b\end{pmatrix}}$					1×2 matrix with elements a and b			\begin{pmatrix} a & b \end{pmatrix}	<*<*a*>,<*b*>*>	(matrix_1:15)
12	12	${\begin{pmatrix}a&b\\c&d\end{pmatrix}}$					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	${\begin{pmatrix}a&b\\c&d\end{pmatrix}}$					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	$a_{ij}$					(i, j)-element of a matrix a			a_{i j}	A*(i,j)	(matrix_1:def 6)
12	15	$A^{t}$					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