Mizar/記号のソースを表示

{{Nav}}

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

|}

{{Nav}}

[[Category:Mizar|きこう]]