コンテンツにスキップ

# Mizar/Q&A/翻訳

< Mizar‎ | Q&A
```reserve k, k1, n, n1, m, m1 for Element of NAT;
reserve X, y for set;
reserve p for Real;
reserve r for real number;
reserve a, a1, a2, b, b1, b2, x, x0, z, z0 for Complex;
reserve s1, s2, s3, seq, seq1 for Complex_Sequence;
```
```reserve Y for Subset of COMPLEX;
```

```reserve f, f1, f2 for PartFunc of COMPLEX,COMPLEX;
```

```reserve Nseq for increasing Seq_of_Nat;
```

Nseqを増加順序立てられた自然数列と置く

```theorem :: 2
0 < r implies s1is convergent;
If 0 < r and for every n holds s1(n) = 1/(n+r) , then s1 is convergent
```

0<r かつ任意のn は s1(n)=1/(n+r)を成立する 、そのときs1は収束する。

```theorem :: 4
seq is constant iff for n,m holds seq.n = seq.m;
```

seq is constant if and only if for every n,m holds seq.n = seq.m.

```theorem :: 5
for n holds (seq*Nseq).n = seq.(Nseq.n);
```

If n ∈ dom(seq ・ Nseq) , then (seq ・ Nseq).n = seq.(Nseq .n)

もし、任意の定義域（seq,Nseq）に含まれるn、そのとき(seq*Nseq).n = seq.(Nseq.n)が成り立つ。

```reserve h for convergent_to_0 Complex_Sequence;
```

hは0への収束する複素列

```reserve c for constant Complex_Sequence;
```

cは定数複素列

```definition
let IT be PartFunc of COMPLEX,COMPLEX;
attr IT is REST-like means:: def 3
for h holds (h")(#)(IT/*h) is convergent & lim ((h")(#)(IT/*h)) = 0;
end;
```

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は(h")(#)(IT/*h)は収束、かつ、lim ((h")(#)(IT/*h)) = 0.

```definition
let IT be PartFunc of COMPLEX,COMPLEX;
attr IT is linear means:: def 4
ex a st for z holds IT/.z = a*z;
end;
```

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.

```theorem :: 6
for g be real number st 0 < g holds
{y where y is Complex : |.y-z0.| < g} is Neighbourhood of z0;
```

Let g be a real number. If 0 < g,

then {y; y is a Complex : |.y-z0.| < g} is a neighbourhood of z0.

ｇは実数とおく。もし、0<g、とすると、そのとき{y|y∈複素数|y-z0|<g}はz0の近傍である。

```definition
let f;
let z0 be Complex;
pred f is_differentiable_in z0 means:: def 6
ex N being Neighbourhood of z0 st N c= dom f & ex L,R st for z be Complex
st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0);
end;
```

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).

ｆ,z0を考える。ｆはz0で微分可能である、同値なのは：存在するz0の近傍Nにおいて、ｆの定義域Ｎ、 かつ、存在するL,Rにおいて、任意のzにおいて、Ｎの要素z0はf/.z-f/.z0 = L/.(z-z0)+R/.(z-z0)に含まれる。

```definition
let f;
let z0 be Complex;
assume f is_differentiable_in z0;
func diff(f,z0) -> Complex means:: def 7
ex N being Neighbourhood of z0 st N c= dom f &
ex L,R st it = L/.1r & for z be Complex
st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0);
end;
```

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∈Nはf/.z-f/.z0 = L/.(z-z0)+R/.(z-z0)をもつ。

```definition
let f;
attr f is differentiable means:: def 8
for x st x in dom f holds f is_differentiable_in x;
end;
```

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で微分可能

```definition
let f,X;
pred f is_differentiable_on X means:: def 9
X c= dom f & f|X is differentiable;
end;
```

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

あるｆ,Xを考える。f はX上で微分可能ということは、fの定義域の部分空間X かつｄf/dXは微分可能である。

```theorem :: 8
f is_differentiable_on X implies X is Subset of COMPLEX;
```

If f is differentiable on X, then X is a subset of COMPLEX

FはX上で微分可能、そのときXは部分複素空間である。

```definition :: complex-membered set
let X be Subset of COMPLEX;
attr X is closed means:: def 10
for s1 be Complex_Sequence
st rng s1 c= X & s1 is convergent holds lim s1 in X;
end;
```

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.

```definition
let X be Subset of COMPLEX;
attr X is open means:: def 11
X` is closed;
end;
```

Let X be a subset of COMPLEX. We say that X is open if and only if: X` is closed.

Xは複素空間部分空間をもってくる。Ｘが開空間というのはX`は閉空間というのと同値である。

```theorem :: 9
for X being Subset of COMPLEX st X is open
for z0 be Complex st z0 in X
ex N being Neighbourhood of z0 st N c= 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.

Ｘを複素部分空間とする。Ｘは開空間と仮定する。 z0は複素空間とする。もし、Xの要素z0、そのとき、存在するz0の近傍Nにおいて、Xの部分空間N

```theorem :: 10
for X being Subset of COMPLEX st X is open
for z0 be Complex st z0 in X holds
ex g be Real st {y where y is Complex : |.y-z0.| < g} c= X;
```

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は複素数の部分集合とする。Ｘを開集合と仮定する。 z0は複素数とする。 Ｘの要素z0と仮定する。そのとき存在する実数ｇにおいて、{y|yの値域は複素数：|y − z0| < g} ⊆ X.

```theorem :: 11
for X being Subset of COMPLEX holds
((for z0 be Complex st z0 in X holds ex N be Neighbourhood of z0 st N c= X)
implies X is open);
```

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.

Ｘは複素数の部分集合。任意の複素数z0において、z0 ∈ X　z0近傍に存在するＮにおいて、そのときＸは開集合である。

```theorem :: 12
for X be Subset of COMPLEX holds X is open iff
for x be Complex st x in X
ex N be Neighbourhood of x st N c= 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の近傍に存在するNにおいてN ⊆ X　と同値である。

```theorem :: 13
for X be Subset of COMPLEX, z0 be Element of COMPLEX, r be Element of REAL st
X = {y where y is Complex : |.y-z0.| < r} holds X is open;
```

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は開集合である。

```theorem :: 14
for X be Subset of COMPLEX,
z0 be Element of COMPLEX,
r be Element of REAL
st X = {y where y is Complex : |.y-z0.| <= r} holds X is closed;
```

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は閉集合である。

```theorem :: 15
f is_differentiable_on Z iff
Z c= dom f & for x st x in Z holds f is_differentiable_in 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で微分可能が成立することと同値である。

```theorem :: 16
f is_differentiable_on Y implies Y is open;
```

If f is differentiable on Y then Y is open.

もし、ｆがY上で微分可能であると、そのときYは開空間である。

```definition
let f, X;
assume f is_differentiable_on X;
func f`|X -> PartFunc of COMPLEX,COMPLEX means:: def 12
dom it = X & for x st x in X holds it/.x = diff(f,x);
end;
```

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 = X　かつ、任意のxにおいて、x ∈ Xがf`|X/.x = diff(f,x)が成り立つ、と定義される。

```registration let seq be non-zero Complex_Sequence, k be Nat;
cluster seq ^\k -> non-zero;
```

```theorem :: 19
(seq-seq1)^\k = (seq^\k)-(seq1^\k);
```

```theorem :: 21
(seq(#)seq1)^\k = (seq^\k)(#)(seq1^\k);
(seq・seq1)^k = seq^k ・seq^k
```

```theorem :: CFDIFF_1:22
for x0 be Complex for N being Neighbourhood of x0 st
f is_differentiable_in x0 & N c= dom f holds
for h,c st rng c = {x0} & rng (h+c) c= N holds
h"(#)(f/*(h+c)-f/*c) is convergent & diff(f,x0) = lim (h"(#)(f/*(h+c)-f/*c));
```

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)).

ｘ0は複素数としＮはx0の近傍。ｆはx0において微分可能、かつ、定義域ｆの部分空間Ｎと仮定する。 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))

```theorem :: CFDIFF_1:23
for f1,f2,x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0
holds f1+f2 is_differentiable_in x0 &
diff(f1+f2,x0) = diff(f1,x0)+diff(f2,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) = f10(x0) + f20(x0).

f1, f2, x0を持ってくる。f1はx0において微分可能、かつ、f2はx0において微分可能と仮定する。 そのとき、f1+f2はx0において微分可能、かつ、(f1 + f2)0(x0) = f10(x0) + f20(x0).

```theorem :: 26
for f1,f2,x0 st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
f1(#)f2 is_differentiable_in x0 &
diff(f1(#)f2,x0) = (f2/.x0)*diff(f1,x0)+(f1/.x0)*diff(f2,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)

```theorem :: 27
for f,Z st Z c= dom f & f|Z = id Z holds
f is_differentiable_on Z & for x st x in Z holds (f`|Z)/.x = 1r;
```

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.

```theorem :: 30
for a,f,Z st Z c= dom (a(#)f) & f is_differentiable_on Z holds
a(#)f is_differentiable_on Z & for x st x in Z holds
((a(#)f)`|Z)/.x = a*diff(f,x);

```

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上で微分可能である。 そのとき、a・fはZ上で微分可能、かつ、任意の全てのxにおいて、Ｚの要素xより((a f)0 |Z)x = a • f0(x)が成立する。

```theorem :: 32
Z c= dom f & f|Z is constant implies
f is_differentiable_on Z & for x st x in Z holds (f`|Z)/.x = 0c;
```

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上で一定、そのとき、ｆはZ上で微分可能、かつ、任意の全てのxにおいてZの要素xにおいて(f`|Z)/.x = 0cが成り立つ。

```theorem :: 33
Z c= dom f & (for x st x in Z holds f/.x = a*x+b) implies
f is_differentiable_on Z & for x st x in Z holds (f`|Z)/.x = a;
```

Suppose Z ⊆ dom f and for every x such that x 2 Z holds fx = a •x+b.

ｆの定義域Ｚ、かつ、z上の任意のｘを仮定すると、fx = a •x+b

Then f is differentiable on Z and for every x such that x ∈ Z holds (f0|Z)x = a.

そのとき、ｆはZ上で微分可能、かつ任意のxにおいて、整数Ｚの要素xにおいて(f0|Z)x = aが成り立つ

```theorem :: 34
for x0 be Complex holds
f is_differentiable_in x0 implies f is_continuous_in x0;
```

For every complex number x0 such that f is differentiable in x0 holds f is continuous in x0.

```theorem :: 35
f is_differentiable_on X implies f is_continuous_on X;
```

If f is differentiable on X, then f is continuous on X.

もし、ｆはX上で微分可能、そのときｆはX上で連続。

```theorem :: 36
f is_differentiable_on X & Z c= X implies f is_differentiable_on Z;
```

If f is differentiable on X and Z ⊆ X, then f is differentiable on Z.

もし、fはX上で微分可能、かつZはXの部分空間、そのとき、fはZ上で微分可能。

```theorem :: 37
seq is convergent implies |.seq.| is convergent;
```

If seq is convergent, then |.seq.| is convergent.

もし、seq は収束すると、seqの絶対値は収束する。

```theorem :: 38
f is_differentiable_in x0 implies ex R st R/.0c = 0c & R is_continuous_in 0c;

```

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で連続。

```reserve k, k1, n, n1, m, m1 for Element of NAT;
reserve X, y for set;
reserve Y for Subset of COMPLEX;
reserve f, f1, f2 for PartFunc of COMPLEX,COMPLEX;
reserve r, p for Real;
reserve a, a1, a2, b, b1, b2, x, x0, y, y0, z, z0 for Complex;
```

```definition let f be PartFunc of COMPLEX,COMPLEX;
func Re f -> PartFunc of COMPLEX,REAL means
:: CFDIFF_2:def 1
dom f = dom it &
for z be Complex st z in dom it holds it.z = Re(f/.z);
end;
```

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).

```definition let f be PartFunc of COMPLEX,COMPLEX;
func Im f -> PartFunc of COMPLEX,REAL means
:: CFDIFF_2:def 2
dom f = dom it & for z be Complex st z in dom it holds it.z=Im (f/.z);
end;
```

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).

```theorem :: CFDIFF_2:2
for f be PartFunc of COMPLEX, COMPLEX,
u,v be PartFunc of REAL 2, REAL,
z0 be Complex,
x0, y0 be Real,
xy0 be Element of REAL 2 st
(for x, y be Real st x+y*＜i> in dom f holds
<*x,y*> in dom u & u.<*x,y*> = (Re f).(x+y*＜i＞)) &
(for x,y be Real st x+y*＜i> in dom f holds
<*x,y*> in dom v & v.<*x,y*> = (Im f).(x+y*＜i＞)) &
z0 = x0+y0*＜i＞ & xy0 = <*x0,y0*> & f is_differentiable_in z0 holds
u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 &
v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 &
Re diff(f,z0) = partdiff(u,xy0,1) & Re diff(f,z0) = partdiff(v,xy0,2) &
Im diff(f,z0) =-partdiff(u,xy0,2) & Im diff(f,z0) = partdiff(v,xy0,1);
```

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.

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において、ｆの定義域の要素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において、ｆの定義域の要素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.

ｆは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は１座標に関して、x1において部分微分可能　かつ　２座標に関してx１で部分微分可能。

(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).

```theorem :: CFDIFF_2:5
for u be PartFunc of REAL 2, REAL,
x0, y0 be Real,
xy0 be Element of REAL 2
st xy0 = <*x0,y0*> & <>*u is_differentiable_in xy0
holds
u is_partial_differentiable_in xy0,1 &
u is_partial_differentiable_in xy0,2 &
<* partdiff(u,xy0,1) *> = diff(<>*u,xy0).(<* 1,0 *>) &
<* partdiff(u,xy0,2) *> = diff(<>*u,xy0).(<* 0,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.

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で部分微分可能。かつ、２座標に関してx1で部分微分可能。

(ii) < partdiff(u, x1, 1) > = < u′(x1) <1, 0>), and

部分微分　　　　　　　　　　　　　、かつ

(iii) < partdiff(u, x1, 2) > = < u′(x1) <0, 1>).

```theorem :: CFDIFF_2:6
for f be PartFunc of COMPLEX, COMPLEX,
u,v be PartFunc of REAL 2, REAL,
z0 be Complex,
x0, y0 be Real,
xy0 be Element of REAL 2 st
(for x,y be Real st <*x,y*> in dom v holds x+y*＜i＞ in dom f) &
(for x,y be Real st x+y*＜i＞ in dom f holds
<*x,y*> in dom u & u.<*x,y*> = (Re f).(x+y*＜i＞)) &
(for x,y be Real st x+y*＜i＞ in dom f holds
<*x,y*> in dom v & v.<*x,y*> = (Im f).(x+y*＜i＞)) &
z0 = x0+y0*＜i＞ & xy0 = <*x0,y0*> &
<>*u is_differentiable_in xy0 &
<>*v is_differentiable_in xy0 &
partdiff(u,xy0,1) = partdiff(v,xy0,2) &
partdiff(u,xy0,2) = -partdiff(v,xy0,1)
holds
f is_differentiable_in z0 &
u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 &
v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 &
Re diff(f,z0) = partdiff(u,xy0,1) & Re diff(f,z0) = partdiff(v,xy0,2) &
Im diff(f,z0) =-partdiff(u,xy0,2) & Im diff(f,z0) = partdiff(v,xy0,1);
```

```Let f be a partial function from C to C,
```

```u, v be partial functions from R2 to R,
```

u, v はR2からRへの部分関数、

```z0 be a complex number,
```

z0は複素数、

```x0, y0 be real numbers, and
```

x0,y0は実数、で、

```x1 be an element of R2.
```

x1はR2の要素である。

```Suppose that for all real numbers x, y such that
<x, y>  ∈ dom v holds x+y•i ∈ dom f and
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) and
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)
and z0 = x0 + y0 • i and x1 = <x0, y0>  and ＜u> is differentiable in x1
and <v>   is differentiable in x1 and partdiff(u, x1, 1) = partdiff(v, x1, 2)
and partdiff(u, x1, 2) = −partdiff(v, x1, 1).
```

```Then
f is differentiable in z0
and u is partially differentiable in x1 w.r.t. 1 coordinate and
partially differentiable in x1 w.r.t. 2 coordinate and
v is partially differentiable in x1 w.r.t. 1 coordinate and
partially differentiable in x1 w.r.t. 2 coordinate and
Re(f′(z0)) =    partdiff(u, x1, 1) and Re(f′(z0))  = partdiff(v, x1, 2) and
Im(f′(z0)) = −partdiff(u, x1, 2) and Im(f′(z0))  = partdiff(v, x1, 1).
```

そのとき、fはz0で微分可能、 かつ、１座標に関してuはx1で部分微分可能、かつ、２座標に関して部分微分可能、 かつ、１座標に関してvはx1で部分微分可能、かつ、２座標に関して部分微分可能、かつ、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).

```omega is the smallest nonempty ordinal number which is a limit.
It is defined in terms of ordinals.
We can think about omega as the set on all natural numbers.
omega is defined in ORDINAL1.
```

オメガは、制限のある、最も小さい空でない序数です。 それは、序列化した項に関して定められます。 私達は、すべての自然数の集合として、オメガについて考えることができます。 オメガは、ORDINAL1で定められています。

```Wikipedia defines Omega:
Transfinite numbers are cardinal numbers or
ordinal numbers that are larger than all finite numbers.
ω (omega) is defined as the lowest transfinite ordinal number.
```

ウィキペディアは、オメガを定めます： 超限数は、すべての有限数より大きい基数または序数です。 ω（オメガ）は、最も低い超限序数と定義されます。

```Omega is an "extension" to the Natural numbers, to get closure under limit
operations, not that dissimilar to the integers (positive and negative)
which are closure of N under subtraction.
```

オメガは自然数への「拡張」です。そして、極限演算で閉じています。そして、それが引き算において、自然数Nの下で閉じている、整数（正と負の）と異なりません。

```definition
func omega -> set means
{} in it & it is limit_ordinal & it is ordinal &
for A st {} in A & A is limit_ordinal holds it c= A;
end;
```

```definition
let A be set;
attr A is natural means
A in omega;
end;
```