コンテンツにスキップ

Mizar/Q&A/翻訳

リンクを追加
出典: フリー教科書『ウィキブックス（Wikibooks）』
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;

複素空間の部分空間をYと置く 

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

複素関数の部分関数をf,f1,f2と置く 

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.

定数seq は　任意のn,m により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は0へ複素連続収束列、かつ、cは複素連続定数列。

複素空間から複素空間への部分関数Aが収束すると呼ぶのは、

それは合計と任意の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.

複素空間から複素空間への部分関数は線形関数と呼ばれている。

存在するaにおいて、任意のzは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.

部分複素空間Xをもってくる.Xは閉である、同値なのは： 任意の列s1は複素列とおいてＸの部分空間である値域s1、かつ、ｓ1が収束することは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;

一時エリア、０でない複素列seqとする、kは自然数列の集まり、０以外の要素seq^k 

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.

任意のｆ,Ｚにおいて、ｆの定義域Z,かつ、f|Z=id Zより、Ｚ上のfで微分可能であり、かつ、任意のｘにおいて,Zの要素xより(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.

任意の複素数x0において、fはx0で微分可能だと成り立つならば、fは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).

任意のｆは複素空間から複素空間への部分関数。 関数実部ｆの部分関数の複素空間から実数空間への場は以下によって定義されている： （定義１）ｆの定義域＝ｆの実数の定義域　かつ　任意の複素数ｚ　において、ｚへのｆの実数部の定義域は　f (z)の実部= (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).

任意のｆは複素関数から複素関数への部分関数。 　複素空間から実数空間への部分関数ｆの虚部の場は以下のように定義される： （定義２）ｆの定義域＝ｆの虚部の定義域　かつ　任意の複素数ｚにおいて、ｚ∈ｆの虚部の定義域は　f (z)の虚部 = (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.

任意のｆはＣからＣへの部分関数、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において、ｆの定義域の要素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.

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

任意(すべて)の実数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). 


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;

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

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

定義 Aは集合 属性Aは自然数 はＡ∈ omegaを意味する 終了

"https://ja.wikibooks.org/w/index.php?title=Mizar/Q%26A/翻訳&oldid=95390" より作成