Mizar/Q&A/翻訳

複素空間の部分空間をYと置く
複素関数の部分関数をf,f1,f2と置く
Nseqを増加順序立てられた自然数列と置く

0<r かつ任意のn は s1(n)=1/(n+r)を成立する 、そのときs1は収束する。
seq is constant if and only if for every n,m holds seq.n = seq.m.
定数seq は 任意のn,m によりseq.n=seq.mが成り立つ。
If n ∈ dom(seq ・ Nseq) , then (seq ・ Nseq).n = seq.(Nseq .n)
もし、任意の定義域(seq,Nseq)に含まれるn、そのとき(seq*Nseq).n = seq.(Nseq.n)が成り立つ。
hは0への収束する複素列
cは定数複素列

In the sequel
h will be a complex sequence convergent to 0 and
c will be a constant complex sequence.
A partial function from COMPLEX to COMPLEX is called a rest if:
it is total and for every h holds (h")(#)(IT/*h) is convergent and lim ((h")(#)(IT/*h)) = 0.
結局、hは0へ複素連続収束列、かつ、cは複素連続定数列。
複素空間から複素空間への部分関数Aが収束すると呼ぶのは、
それは合計と任意のhは(h")(#)(IT/*h)は収束、かつ、lim ((h")(#)(IT/*h)) = 0.

A partial function from COMPLEX to COMPLEX called a line function if:
it is total there exists r such that for every z holds it/.z = a*z.
複素空間から複素空間への部分関数は線形関数と呼ばれている。
存在するaにおいて、任意のzはit/.z=a*zと成り立つ。
Let g be a real number. If 0 < g,
then {y; y is a Complex : |.y-z0.| < g} is a neighbourhood of z0.
gは実数とおく。もし、0<g、とすると、そのとき{y|y∈複素数|y-z0|<g}はz0の近傍である。
Let us consider f, z0. We say that f is differentiable in z0 if and only if:
there exists a neighbourhood N of z0 such that N ⊆ domf and there exist
L, R such that for every z such that z ∈ N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0).
f,z0を考える。fはz0で微分可能である、同値なのは:存在するz0の近傍Nにおいて、fの定義域N、 かつ、存在するL,Rにおいて、任意のzにおいて、Nの要素z0はf/.z-f/.z0 = L/.(z-z0)+R/.(z-z0)に含まれる。
Let us consider f, z0. Let us assume that f is differentiable in z0. The functor f′(z0) yields a Complex number and is defined as follows: there exists a neighbourhood N of z0 such that N ⊆ domf and there exist L, R such that f′(z0) = L/.(1r) and for every z such that z ∈ N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0).
f,z0と置くとz0点でfは微分可能であると仮定する。 以下より、関数f′(z0)領域は複素数であると定義できる。: あるz0の近傍Nが存在する。 fの定義域の部分空間Nと 存在するL,R においてf′(z0) = L/.(1r)かつ任意のzにおいてz∈Nはf/.z-f/.z0 = L/.(z-z0)+R/.(z-z0)をもつ。
Let f. We say that f is differentiable if and only if: for x such that x in dom f holds f is_differentiable_in x.
fをとる、fは微分可能とする。 任意のx xは定義域を持ち、fはxで微分可能
Let us consider f, X. We say that f is differentiable on X if and only if: X ⊆ domf and for every x such that x ∈ dom f holds f|X is differentiable
あるf,Xを考える。f はX上で微分可能ということは、fの定義域の部分空間X かつdf/dXは微分可能である。
If f is differentiable on X, then X is a subset of COMPLEX
FはX上で微分可能、そのときXは部分複素空間である。
Let X be Subset of COMPLEX. We say that X is closed if and only if: For every sequence s1 be Complex_Sequence such that rng s1 ⊆ X and s1 is convergent holds lim s1 ∈ X.
部分複素空間Xをもってくる.Xは閉である、同値なのは: 任意の列s1は複素列とおいてXの部分空間である値域s1、かつ、s1が収束することはlim s1 ∈Xを有する。
Let X be a subset of COMPLEX. We say that X is open if and only if: X` is closed.
Xは複素空間部分空間をもってくる。Xが開空間というのはX`は閉空間というのと同値である。
Let X be a subset of COMPLEX. Suppose X is open. Let z0 be a Complex. If z0 ∈ X, then there exists a neighbourhood N of z0 such that N ⊆ X.
Xを複素部分空間とする。Xは開空間と仮定する。 z0は複素空間とする。もし、Xの要素z0、そのとき、存在するz0の近傍Nにおいて、Xの部分空間N

Let X be a subset of C. Suppose X is open. Let z0 be a complex number. Suppose z0 ∈ X. Then there exists a real number g such that {y; y ranges over complex numbers: |y − z0| < g} ⊆ X.
over complex numberではなくin complex numberではないでしょうか???.
Xは複素数の部分集合とする。Xを開集合と仮定する。 z0は複素数とする。 Xの要素z0と仮定する。そのとき存在する実数gにおいて、{y|yの値域は複素数:|y − z0| < g} ⊆ X.
Let X be a subset of C. Suppose that for every complex number z0 such that z0 ∈ X there exists a neighbourhood N of z0 such that N ⊆X. Then X is open.
Xは複素数の部分集合。任意の複素数z0において、z0 ∈ X z0近傍に存在するNにおいて、そのときXは開集合である。
Let X be a subset of C. Then X is open if and only if for every complex number x such that x ∈ X there exists a neighbourhood N of x such that N ⊆ X.
Xは複素数の部分集合と置く、そのとき、Xは開集合であることは、全ての複素数xにおいてx ∈ X、xの近傍に存在するNにおいてN ⊆ X と同値である。
Let X be a subset of C, z0 be an element of C, and r be an element of R. If X = {y; y ranges over complex numbers: |y − z0| < r}, then X is open.
Xは複素数の部分集合、z0は複素数の要素、rは実数の要素と置く。 もし、X={y|yの値域は複素数:|y-z0|<r}、そのときXは開集合である。
Let X be a subset of C, z0 be an element of C, and r be an element of R. If X = {y; y ranges over complex numbers: |y − z0| <= r}, then X is closed.
Xは複素数の部分集合、z0は複素数の要素、rは実数の要素と置く。 もし、X={y|yの値域は複素数:|y-z0|<=r}、そのときXは閉集合である。
f is differentiable on Z if and only if Z ⊆ domf and for every x such that x ∈ Z holds f is differentiable in x.
fが整数空間上で微分可能であるとは、Z⊆dom f かつ、任意のxにおいて、x∈Zはxで微分可能が成立することと同値である。
If f is differentiable on Y then Y is open.
もし、fがY上で微分可能であると、そのときYは開空間である。
Let us consider f, X. Let us assume that f is differentiable on X. The functor f`|X yielding a partial function from COMPLEX to COMPLEX is defined by: dom f`|X = X and for every x such that x ∈ X holds f`|X/.x = diff(f,x).
f、xを考える。 fはX上で微分可能と仮定する。 部分関数である関数f`|Xの複素空間から複素空間への意味は 定義域f`|X = X かつ、任意のxにおいて、x ∈ Xがf`|X/.x = diff(f,x)が成り立つ、と定義される。
一時エリア、0でない複素列seqとする、kは自然数列の集まり、0以外の要素seq^k
Let x0 be a complex number and N be a neighbourhood of x0. Suppose f is differentiable in x0 and N ⊆ dom f. Let given h, c. Suppose rng c = {x0} and rng(h + c) ⊆ N. Then h" (f • (h + c) − f • c) is convergent and f0(x0) = lim(h" (f • (h + c) − f • c)).
x0は複素数としNはx0の近傍。fはx0において微分可能、かつ、定義域fの部分空間Nと仮定する。 h,cを持ってくる。rng c = {x0} かつ rng(h + c) ⊆ N。そのときh" (f • (h + c) − f • c) は収束し、かつ、diff(f,x0) = lim(h" (f • (h + c) − f • c))
Let given f1, f2, x0. Suppose f1 is differentiable in x0 and f2 is differentiable in x0. Then f1 + f2 is differentiable in x0 and (f1 + f2)0(x0) = f10(x0) + f20(x0).
f1, f2, x0を持ってくる。f1はx0において微分可能、かつ、f2はx0において微分可能と仮定する。 そのとき、f1+f2はx0において微分可能、かつ、(f1 + f2)0(x0) = f10(x0) + f20(x0).
Let given f1, f2, x0. Suppose f1 is differentiable in x0 and f2 is differentiable in x0. Then f1 f2 is differentiable in x0 and (f1 f2)0(x0) = (f2)x0 • f10(x0) + (f1)x0 • f20(x0).
f1, f2, x0を持ってくる。f1はx0において微分可能、かつ、f2はx0において微分可能と仮定する。 そのとき、f1・f2はx0において微分可能、かつ、(f1 f2)0(x0) = (f2)x0 • f10(x0) + (f1)x0 • f20(x0)
For all f, Z such that Z ⊆ dom f and f | Z = idZ holds f is differentiable on Z and for every x such that x 2 Z holds (f0 | Z)x = 1C.
任意のf,Zにおいて、fの定義域Z,かつ、f|Z=id Zより、Z上のfで微分可能であり、かつ、任意のxにおいて,Zの要素xより(f0 | Z)x = 1Cが成立する。
Let given a, f, Z. Suppose Z ⊆ dom(a f) and f is differentiable on Z. Then a f is differentiable on Z and for every x such that x ∈ Z holds ((a f)0 |Z)x = a • f0(x).
a,f,Zをもってくる。定義域(a f)の部分集合Zを仮定し、かつ、fはZ上で微分可能である。 そのとき、a・fはZ上で微分可能、かつ、任意の全てのxにおいて、Zの要素xより((a f)0 |Z)x = a • f0(x)が成立する。
If Z ⊆ domf and f is a constant on Z, then f is differentiable on Z and for every x such that x ∈ Z holds (f`|Z)/.x = 0c.
もし、fの定義域Z,かつ,fはZ上で一定、そのとき、fはZ上で微分可能、かつ、任意の全てのxにおいてZの要素xにおいて(f`|Z)/.x = 0cが成り立つ。
Suppose Z ⊆ dom f and for every x such that x 2 Z holds fx = a •x+b.
fの定義域Z、かつ、z上の任意のxを仮定すると、fx = a •x+b
Then f is differentiable on Z and for every x such that x ∈ Z holds (f0|Z)x = a.
そのとき、fはZ上で微分可能、かつ任意のxにおいて、整数Zの要素xにおいて(f0|Z)x = aが成り立つ
For every complex number x0 such that f is differentiable in x0 holds f is continuous in x0.
任意の複素数x0において、fはx0で微分可能だと成り立つならば、fはx0で連続
If f is differentiable on X, then f is continuous on X.
もし、fはX上で微分可能、そのときfはX上で連続。
If f is differentiable on X and Z ⊆ X, then f is differentiable on Z.
もし、fはX上で微分可能、かつZはXの部分空間、そのとき、fはZ上で微分可能。
If seq is convergent, then |.seq.| is convergent.
もし、seq は収束すると、seqの絶対値は収束する。
If f is differentiable in x0, then there exists R such that R(0) = 0 and R is continuous in 0.
もし、fはx0で微分可能、そのとき存在するRにおいてR(0)=0 かつRは0で連続。

:: CFDIFF_2:def 1
Let f be a partial function from C to C. The functor Re f yielding a partial function from C to R is defined by: (Def. 1) dom f = dom Re f and for every complex number z such that z ∈ dom Re f holds Re f (z) = Re (fz).
任意のfは複素空間から複素空間への部分関数。 関数実部fの部分関数の複素空間から実数空間への場は以下によって定義されている: (定義1)fの定義域=fの実数の定義域 かつ 任意の複素数z において、zへのfの実数部の定義域は f (z)の実部= (fz)の実部に含まれる
:: CFDIFF_2:def 2
Let f be a partial function from C to C. The functor Im f yielding a partial function from C to R is defined as follows: (Def. 2) dom f = dom Im f and for every complex number z such that z ∈ dom Im f holds Im f (z) = Im (fz).
任意のfは複素関数から複素関数への部分関数。 複素空間から実数空間への部分関数fの虚部の場は以下のように定義される: (定義2)fの定義域=fの虚部の定義域 かつ 任意の複素数zにおいて、z∈fの虚部の定義域は f (z)の虚部 = (fz)の虚部 に含まれる。
Let f be a partial function from C to C, u, v be partial functions from R2 to R, z0 be a complex number, x0, y0 be real numbers, and x1 be an element of R2.
任意のfはCからCへの部分関数、u,vはR2からRへの部分関数、z0は複素数、x0,y0は実数、そして、x1はR2の要素である。
Suppose that
以下の仮定をする。
(i) for all real numbers x, y such that x+y • i ∈ dom f holds <x, y> ∈ dom u and u<x, y> = Re(f)(x + y • i),
(i)任意の実数x,yにおいて、fの定義域の要素x+y・iは uの定義域の要素<x, y> かつ u<x, y> = 実数部(f)(x + y • i)に含まれる。
(ii) for all real numbers x, y such that x+y • i ∈ dom f holds <x, y> ∈ dom v and v<x, y> = Im(f)(x + y • i),
(ii)任意の実数x,yにおいて、fの定義域の要素x+y・iは vの定義域の要素<x, y> かつ v<x, y> = 虚数部(f)(x + y • i)に含まれる。
(iii) z0 = x0 + y0 • i,
(iv) x1 = <x0, y0> , and
かつ
(v) f is differentiable in z0.
fはz0で微分可能。
Then
そのとき、
(vi) u is partially differentiable in x1 w.r.t. 1 coordinate and partially differentiable in x1 w.r.t. 2 coordinate,
uは1座標に関して、x1において部分微分可能 かつ 2座標に関してx1で部分微分可能。
(vii) v is partially differentiable in x1 w.r.t. 1 coordinate and partially differentiable in x1 w.r.t. 2 coordinate,
(viii) Re(f ′(z0)) = partdiff(u, x1, 1),
(ix) Re(f ′(z0)) = partdiff(v, x1, 2),
(x) Im(f ′(z0)) = − partdiff(u, x1, 2), and
(xi) Im(f ′(z0)) = partdiff(v, x1, 1).
Let u be a partial function from R2 to R, x0, y0 be real numbers, and x1 be an element of R2. Suppose x1 = <x0, y0> and < u > is differentiable in x1.
任意のuはR2からRへの部分関数、x0,y0は実数、かつ、x1はR2の要素。 x1 = <x0, y0> かつ < u >はx1で微分可能であることを仮定する。
Then
そのとき、
(i) u is partially differentiable in x1 w.r.t. 1 coordinate and partially differentiable in x1 w.r.t. 2 coordinate,
1座標に関して、uはx1で部分微分可能。かつ、2座標に関してx1で部分微分可能。
(ii) < partdiff(u, x1, 1) > = < u′(x1) <1, 0>), and
部分微分 、かつ
(iii) < partdiff(u, x1, 2) > = < u′(x1) <0, 1>).

任意のfはcからCへの部分関数
u, v はR2からRへの部分関数、
z0は複素数、
x0,y0は実数、で、
x1はR2の要素である。
任意(すべて)の実数x,yを仮定すると、定義域vの要素<x,y>は定義域fの要素x+y•iに含まれる。かつ、任意の実数x,yにおいて、fの定義域の要素x+y•i はuの定義域の要素<x, y>に含まれる、かつ、 u<x, y> = Re(f)(x+y • i) 、かつ、 任意の実数x,yにおいて、fの定義域の要素x+y•i はvの定義域の要素<x, y>、かつ、v<x, y> = Im(f)(x+y•i)、かつ、z0 = x0 + y0 • i 、かつ、 x1 = <x0, y0>、かつ、<u> はx1で微分可能、かつ、 <v>は x1 において微分可能、かつ、 partdiff(u, x1, 1) = partdiff(v, x1, 2)、かつ、partdiff(u, x1, 2) = −partdiff(v, x1, 1).

そのとき、fはz0で微分可能、 かつ、1座標に関してuはx1で部分微分可能、かつ、2座標に関して部分微分可能、 かつ、1座標に関してvはx1で部分微分可能、かつ、2座標に関して部分微分可能、かつ、Re(f′(z0)) = partdiff(u, x1, 1) かつ Re(f′(z0)) = partdiff(v, x1, 2) and Im(f′(z0)) = −partdiff(u, x1, 2) かつ Im(f′(z0)) = partdiff(v, x1, 1).
オメガは、制限のある、最も小さい空でない序数です。 それは、序列化した項に関して定められます。 私達は、すべての自然数の集合として、オメガについて考えることができます。 オメガは、ORDINAL1で定められています。

ウィキペディアは、オメガを定めます: 超限数は、すべての有限数より大きい基数または序数です。 ω(オメガ)は、最も低い超限序数と定義されます。
オメガは自然数への「拡張」です。そして、極限演算で閉じています。そして、それが引き算において、自然数Nの下で閉じている、整数(正と負の)と異なりません。

定義 関数 omega 集合の意味することは、 空集合 かつ 極限序数 かつ 序数 かつ 任意のAにおいて、空集合∈A かつ Aは極限序数 は omega⊆A をもつ。 終了
定義 Aは集合 属性Aは自然数 はA∈ omegaを意味する 終了