# Mizar/記号

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 ${\displaystyle \notin }$ ∈ の否定 「￢(x ∈ S)」を「x ? S」と書く。 \not\in
2 1.3 ? ${\displaystyle \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 ? ${\displaystyle \varsubsetneqq }$ \varsubsetneqq
2 5.3 ? ${\displaystyle \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 ? ${\displaystyle \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 ${\displaystyle ()^{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 ${\displaystyle \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 ω ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ? ${\displaystyle \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 ${\displaystyle 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 ${\displaystyle 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 ${\displaystyle {\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 ${\displaystyle ()^{2}}$ squre (of a number) ^2 ^2 (square_1:def 3) a^2 [the square of a]
7 13.1 ${\displaystyle ()^{2}}$ squre (of a number) ^2 sqr (square_1:def 3) a^2 [the square of a]
7 14 ${\displaystyle 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 ${\displaystyle 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 ${\displaystyle 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 ${\displaystyle 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 ${\displaystyle 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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle \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 ${\displaystyle 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 ${\displaystyle 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 ${\displaystyle ({\vec {a}})}$ 1×…matrix a (line vector) (\vec{a}) <*a*> (matrix_1:11)
12 4 ${\displaystyle ({\vec {a}})}$ 1×ｎmatrix a (line vector) (\vec{a}) <*a*> st width <*a*> = n (matrix_1:11;matrix_1: def 4)
12 4 ${\displaystyle ({\vec {a}})^{t}}$ …×1 matrix a (column vector) (\vec{a})^t <*a*>@? (matrix_1:11; matrix_1: def 7 )
12 5 ${\displaystyle ({\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 ${\displaystyle {\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 ${\displaystyle {\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 ${\displaystyle {\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 ${\displaystyle {\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 ${\displaystyle (a)}$ 1×1 matrix with element a matrix (a) <*<*a*>*> (matrix_1:15)
12 11 ${\displaystyle {\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 ${\displaystyle {\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 ${\displaystyle {\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 ${\displaystyle a_{ij}}$ (i, j)-element of a matrix a a_{i j} A*(i,j) (matrix_1:def 6)
12 15 ${\displaystyle 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

Tの要素、範囲 the carrier of T the carrier of T
Aの補集合 {}A
{A} 集合A [#]A

relation 関係 relation
reflexive 反射的 reflexive
symmetric 対称的 symmetric
transitive 推移的 transitive
antisymmetric 反対称的 antisymmetric

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

then + thus hence
IDENTITY RELATION 同値関係 id

∂A 外包 boundary TOPS_1 A is boundary
X1-X2| X1,X2の距離 dist(X1,X2) JGRAPH_1 dist(X1,X2)

bi i番目の要素 b/.i BINARITH