::
:: On n-dimensional Real Spaces and n-dimensional Complex Spaces I
:: 19. Nov. 2020
:: Yatsuka Nakamura
environ
vocabularies TARSKI, NUMBERS, NAT_1, FINSEQ_2, FINSEQ_1, SUBSET_1, SQUARE_1,
VALUED_0, CARD_1, XXREAL_0, XCMPLX_0, FUNCT_1, FUNCT_2, FUNCT_7,
XBOOLE_0, RVSUM_1, COMPLEX1, RELAT_1, REAL_1, ARYTM_1, MOMENTM1;
notations TARSKI, XBOOLE_0, VALUED_0, FUNCT_1, FUNCT_2, ORDINAL1, CARD_1,
NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, FINSEQ_1, FINSEQ_2, DOMAIN_1,
RELAT_1, XXREAL_0, SUBSET_1, EUCLID;
constructors COMPLEX1, FINSEQOP, TOPMETR, EUCLID;
registrations RELSET_1, NUMBERS, XREAL_0, FINSEQ_2, RVSUM_1, ORDINAL1,
COMPLEX1, XCMPLX_0;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI;
equalities EUCLID, FINSEQ_1, FINSEQ_2;
expansions TARSKI, XBOOLE_0;
theorems FINSEQ_1, FINSEQ_2, FUNCT_1, FUNCT_2, TARSKI, COMPLEX1, FUNCOP_1,
ORDINAL1, NUMBERS, XBOOLE_1;
begin
reserve a,b,c,d for Real;
reserve x,y,x3,y3,X,z,Y,Z,V for set;
theorem Th1:
(REAL) c= COMPLEX by NUMBERS:11;
theorem ::CCD20:
* in COMPLEX;
theorem ::CCD21:
***** = -1r by COMPLEX1:18;
theorem Th4:
not ** in REAL by COMPLEX1:7;
theorem ::CCC21:
(REAL) c< COMPLEX by Th4,Th1;
theorem
REAL* is FinSequenceSet of REAL;
theorem
COMPLEX* is FinSequenceSet of COMPLEX;
theorem Th8: REAL* is FinSequenceSet of COMPLEX
by FINSEQ_2:91,Th1;
theorem
REAL* c= COMPLEX* by FINSEQ_2:90,Th8;
definition
let n be Nat;
func COMPLEX n -> FinSequenceSet of COMPLEX equals
n-tuples_on COMPLEX;
coherence;
end;
registration
let n be Nat;
cluster COMPLEX n -> non empty;
coherence;
end;
registration
let n be Nat;
cluster -> n-element for Element of COMPLEX n;
coherence;
end;
theorem
for n being Nat holds
REAL n = n-tuples_on REAL;
theorem
for n being Nat holds
COMPLEX n = n-tuples_on COMPLEX;
registration
let n be Nat;
cluster -> n-element for Element of (COMPLEX n);
coherence;
end;
theorem
for n being Nat holds
REAL n = n-tuples_on REAL;
theorem
for n being Nat holds
COMPLEX n = n-tuples_on COMPLEX;
theorem
for n being Nat holds
REAL n is FinSequenceSet of REAL;
theorem
for n being Nat holds
COMPLEX n is FinSequenceSet of COMPLEX;
registration
let n be Nat;
cluster COMPLEX n -> non empty;
coherence;
end;
registration
let n be Nat;
cluster -> n-element for Element of COMPLEX n;
coherence;
end;
theorem ::CCC22:
for n being Nat holds
COMPLEX n = n-tuples_on COMPLEX;
reserve z for Complex;
reserve x,x3,y,z,P,Q,X,Y,Z for set;
theorem Th17:
for n being Nat holds
n-tuples_on REAL = Funcs(Seg n,REAL) by FINSEQ_2:93;
theorem Th18:
for n being Nat holds
n-tuples_on COMPLEX = Funcs(Seg n,COMPLEX) by FINSEQ_2:93;
theorem Th19:
for x being object,n being Nat holds
x in Funcs(Seg n,REAL) iff ex f being Function st x = f &
dom f = Seg n & rng f c= REAL by FUNCT_2:def 2;
theorem Th20:
for x being object,n being Nat holds
x in Funcs(Seg n,COMPLEX) iff ex f being Function st x = f &
dom f = Seg n & rng f c= COMPLEX by FUNCT_2:def 2;
theorem Th21:
for n being Nat holds
n-tuples_on COMPLEX = Funcs(Seg n,COMPLEX) by FINSEQ_2:93;
theorem Th22:for n being Nat holds
Funcs(Seg n,REAL)c= Funcs(Seg n,COMPLEX)
proof
let n be Nat;
thus Funcs(Seg n,REAL)c= Funcs(Seg n,COMPLEX)
proof
let x3 be object;
assume x3 in Funcs(Seg n,REAL);then
consider f be Function such that
A1: x3 = f &
dom f = Seg n & rng f c= REAL by Th19;
thus x3 in Funcs(Seg n,COMPLEX) by Th1,Th20,XBOOLE_1:1,A1; ::CCC20,
end;
end;
theorem Th23:
for n being Nat holds (n-tuples_on REAL)
c= (n-tuples_on COMPLEX)
proof
let n be Nat;
now let x3 being object;
assume A1: x3 in (n-tuples_on REAL);
A2: Funcs(Seg n,REAL) c= Funcs(Seg n,COMPLEX) by Th22;
x3 in Funcs(Seg n,REAL)by Th17,A1;then
x3 in Funcs(Seg n,COMPLEX)by A2;
hence x3 in (n-tuples_on COMPLEX)by Th21;
end;
hence thesis;
end;
theorem
for n being Nat holds (REAL n) c= (COMPLEX n) by Th23;
reserve f for real-valued FinSequence;
definition
let n be Nat;
func I*n -> FinSequence equals
n |-> In(1,REAL);
correctness;
end;
definition
let n be Nat;
func i*n -> complex-valued FinSequence equals
n |-> In(**,COMPLEX);
correctness;
end;
theorem ::CCC525:
for n being Nat holds
i*n is Element of COMPLEX n;
theorem ::CCC526:
for n being Nat st 1 <= n
holds i*n in COMPLEX n;
registration
let n be Nat;
cluster -> n-element for Element of COMPLEX n;
correctness;
end;
theorem Th27:
for n being Nat st 1 <= n
holds rng (i*n) = {**} &
ex f2 being Function st
dom f2 = Seg n & rng f2 c= COMPLEX
proof
let n be Nat;
assume A1: 1 <= n;
A2: 1 in Seg n by A1;
A3: n is Element of NAT by ORDINAL1:def 12;
for A being set, p being FinSequence of
A holds p in n -tuples_on A iff len p = n by FINSEQ_2:133,A3;then
A4: for p being FinSequence of COMPLEX holds
( p in n -tuples_on COMPLEX iff len p = n );
A5: i* n in n -tuples_on COMPLEX iff len (i* n) = n by A4;
A6: len (i* n) = n by A5;
A7: Seg len (i* n) = dom (i* n) by FINSEQ_1:def 3;
A8: len (i* n) =n by A6;then
A9: dom (i*n) = Seg n by A7;
1 in { k where k is Nat : ( 1 <= k & k <= n ) } by A2;then
A10: 1 in Seg n;then
A11: 1 in dom (i*n) by A9;
A12: (n |-> In(**,COMPLEX)).1 = In(**,COMPLEX)by A10,FUNCOP_1:7;
reconsider p = (n |-> In(**,COMPLEX)) as FinSequence;
A13: Seg len p = dom p by FINSEQ_1:def 3;
p.1 = In(**,COMPLEX) by A12; then
A14: (n |-> **).1
= In(**,COMPLEX)
.= ** ;
A15: (n |-> In(**,COMPLEX)).1= ** by A14;
rng (n |-> In(**,COMPLEX))= {**}
proof
A16: rng(n |-> In(**,COMPLEX)) c= {**}
proof let y3 be object;
assume y3 in rng(n |-> In(**,COMPLEX));then
consider x3 being object such that
A17: x3 in dom (n |-> In(**,COMPLEX))
& (n |-> In(**,COMPLEX)).x3 = y3 by FUNCT_1:def 3;
x3 in dom (n |-> In(**,COMPLEX)) by A17;then
x3 in Seg n by A13,A8;then
x3 in Seg n ;then
A18: (n |-> In(**,COMPLEX)).x3 = In(**,COMPLEX)by FUNCOP_1:7;
(n |-> **).x3
= In(**,COMPLEX) by A18
.= ** ;
then
A19: (n |-> In(**,COMPLEX)).x3= **;
A20: x3 in dom (n |-> In(**,COMPLEX))
& (n |-> In(**,COMPLEX)).x3= y3 by A17;
y3= ** by A20,A19;
hence y3 in {**} by TARSKI:def 1;
end;
{**} c= rng(n |-> In(**,COMPLEX))
proof let y3 be object;
assume y3 in {**};then
A21: y3= ** by TARSKI:def 1;
A22: 1 in dom (n |-> In(**,COMPLEX)) by A11;
1 in dom (n |-> In(**,COMPLEX))
& (n |-> In(**,COMPLEX)).1= y3 by A21,A22,A15;
hence y3 in rng(n |-> In(**,COMPLEX)) by FUNCT_1:def 3;
end;
hence thesis by A16;
end;
hence rng (i*n) = {**} &
ex f2 being Function st
dom f2 = Seg n & rng f2 c= COMPLEX by A9;
end;
theorem Th28:
for n being Nat
holds Funcs(Seg n,REAL)c= Funcs(Seg n,COMPLEX) by Th22;
theorem Th29:
for n being Nat st 1 <= n
holds i* n in Funcs(Seg n,COMPLEX)
& not i* n in Funcs(Seg n,REAL)
proof let n be Nat;
assume A1: 1 <= n;
n-tuples_on COMPLEX = Funcs(Seg n,COMPLEX) by FINSEQ_2:93;then
A2: i* n in Funcs(Seg n,COMPLEX);
1 in { k where k is Nat: 1 <= k & k <= n } by A1;then
A3: 1 in Seg n;
A4: not ** in REAL by Th4;
now assume A5: i* n in Funcs(Seg n,REAL);
consider f be Function such that
A6: (i* n) = f & dom f = Seg n & rng f c= REAL by A5,FUNCT_2:def 2;
1 in Seg n by A3;then
A7: (i* n).1 in rng (i* n) by A6,FUNCT_1:def 3;
(i*n).1 in {**} by A7,A1,Th27;then
A8: (i*n).1 = ** by TARSKI:def 1;
** in REAL by A8,A7,A6;
hence contradiction by A4;
end;then
not i* n in Funcs(Seg n,REAL);
hence thesis by A2;
end;
theorem Th30:
for n being Nat st 1 <= n
holds Funcs(Seg n,REAL)c< Funcs(Seg n,COMPLEX)
proof let n be Nat;
assume A1: 1 <= n;
A2: Funcs(Seg n,REAL)c= Funcs(Seg n,COMPLEX)by Th28;
now assume A3: Funcs(Seg n,REAL)= Funcs(Seg n,COMPLEX);
i* n in Funcs(Seg n,COMPLEX) by Th29,A1;
hence contradiction by A3,Th29,A1;
end;
hence thesis by A2;
end;
theorem Th31:
for n being Nat st n>=1
holds (n-tuples_on REAL) c< (n-tuples_on COMPLEX)
proof let n be Nat;
assume A1: n>=1;
A2: Funcs(Seg n,REAL)=(n-tuples_on REAL) by Th17;
Funcs(Seg n,COMPLEX)=(n-tuples_on COMPLEX) by Th18;
hence thesis by A1,A2,Th30;
end;
theorem
for n being Nat st n>=1
holds (REAL n) c< (COMPLEX n) by Th31;
*