environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, SEQ_1, ORDINAL2, NAT_1, ARYTM_3, XXREAL_0, REAL_1, CARD_1, ARYTM_1, MEMBERED, XXREAL_2, COMPLEX1, TARSKI, XBOOLE_0, SEQ_2, FUNCT_1, VALUED_0, RELAT_1, FUNCOP_1, VALUED_1, SQUARE_1, SEQM_3, SEQ_4, BINOP_1, BINOP_2, FINSEQOP, XCMPLX_0, COMPLSP1, FINSEQ_1, ZFMISC_1, FINSEQ_2, CARD_3, RVSUM_1, RCOMP_1, SETFAM_1, METRIC_1, FINSET_1, ORDINAL4, PARTFUN1, GOBOARD2, MEMBER_1, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, CARD_1, FINSET_1, MEMBERED, ORDINAL1, NUMBERS, XXREAL_2, XCMPLX_0, XXREAL_0, XREAL_0, SETFAM_1, REAL_1, SQUARE_1, COMPLEX1, FUNCT_1, RELSET_1, PARTFUN1, SEQ_1, COMSEQ_2, SEQ_2, SEQM_3, FUNCT_2, BINOP_1, BINOP_2, FINSEQ_1, FUNCOP_1, NAT_1, VALUED_0, VALUED_1, MEMBER_1, RVSUM_1, FINSEQ_2, RECDEF_1, FINSEQOP;
definitions XBOOLE_0, TARSKI, SEQ_2, FINSEQ_1, XXREAL_2, FINSEQOP;
theorems NAT_1, SEQ_1, SEQ_2, SEQM_3, AXIOMS, FUNCT_1, FUNCT_2, ABSVALUE, TARSKI, RELAT_1, RELSET_1, XREAL_0, XBOOLE_1, SUBSET_1, XCMPLX_0, MEMBERED, XREAL_1, FUNCOP_1, COMPLEX1, XXREAL_0, ORDINAL1, SQUARE_1, XXREAL_2, VALUED_0, BINOP_2, SETWISEO, FINSEQOP, BINOP_1, ZFMISC_1, VALUED_1, FINSEQ_1, FINSEQ_2, RVSUM_1, XBOOLE_0, FINSEQ_3, CARD_1, CARD_2, FINSEQ_4, MEMBER_1, NUMBERS;
schemes NAT_1, RECDEF_1, SEQ_1, SUBSET_1, FUNCT_2, FRAENKEL, BINOP_2, DOMAIN_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, FUNCOP_1, SEQ_2, FINSET_1, BINOP_2, FUNCT_1, FINSEQ_2, SUBSET_1, NAT_1, RELAT_1, FINSEQ_1, CARD_1, MEMBER_1, SQUARE_1, RVSUM_1, XCMPLX_0, SEQ_1;
constructors HIDDEN, FUNCOP_1, REAL_1, NAT_1, COMPLEX1, PARTFUN1, SEQ_2, SEQM_3, SQUARE_1, VALUED_1, RECDEF_1, XXREAL_2, FINSET_1, RELSET_1, BINOP_1, BINOP_2, SETWISEO, FINSEQOP, ZFMISC_1, RVSUM_1, MEMBER_1, COMSEQ_2, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities COMPLEX1, FINSEQ_1, SQUARE_1, SUBSET_1, VALUED_1;
expansions XBOOLE_0, TARSKI, SEQ_2, XXREAL_2, FINSEQOP, VALUED_1;
theorem Th1:
for
X,
Y being
Subset of
REAL st ( for
r,
p being
Real st
r in X &
p in Y holds
r < p ) holds
ex
g being
Real st
for
r,
p being
Real st
r in X &
p in Y holds
(
r <= g &
g <= p )
theorem Th3:
for
r being
Real ex
n being
Nat st
r < n
Lm1:
for r being Real
for X being non empty real-membered set st ( for s being Real st s in X holds
s >= r ) & ( for t being Real st ( for s being Real st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X
Lm2:
for X being non empty real-membered set
for r being Real st ( for s being Real st s in X holds
s <= r ) & ( for t being Real st ( for s being Real st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X
reconsider zz = 0 as Nat ;
Lm3:
for c, c9 being Element of COMPLEX holds (multcomplex [;] (c,(id COMPLEX))) . c9 = c * c9
Lm4:
for n being Nat
for z being Element of COMPLEX n holds dom z = Seg n
Lm5:
for n being Nat holds - (0c n) = 0c n
Lm6:
for n being Nat
for z, z1, z2 being Element of COMPLEX n st z1 + z = z2 + z holds
z1 = z2
definition
let n be
Nat;
let A,
B be
Subset of
(COMPLEX n);
deffunc H1(
Element of
COMPLEX n,
Element of
COMPLEX n)
-> Element of
REAL =
In (
|.($1 - $2).|,
REAL);
deffunc H2(
Element of
COMPLEX n,
Element of
COMPLEX n)
-> Real =
|.($1 - $2).|;
defpred S1[
set ,
set ]
means ( $1
in A & $2
in B );
reconsider X =
{ H1(x,z) where x, z is Element of COMPLEX n : S1[x,z] } as
Subset of
REAL from DOMAIN_1:sch 9();
A1:
for
z1,
z2 being
Element of
COMPLEX n holds
H1(
z1,
z2)
= H2(
z1,
z2)
;
A2:
{ H1(z1,z2) where z1, z2 is Element of COMPLEX n : S1[z1,z2] } = { H2(z1,z2) where z1, z2 is Element of COMPLEX n : S1[z1,z2] }
from FRAENKEL:sch 7(A1);
existence
ex b1 being Real st
for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
b1 = lower_bound X
uniqueness
for b1, b2 being Real st ( for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
b1 = lower_bound X ) & ( for X being Subset of REAL st X = { |.(x - z).| where x, z is Element of COMPLEX n : ( x in A & z in B ) } holds
b2 = lower_bound X ) holds
b1 = b2
end;
defpred S1[ Nat] means for R being finite Subset of REAL st R <> {} & card R = $1 holds
( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R );
Lm7:
S1[ 0 ]
;
Lm8:
for n being Nat st S1[n] holds
S1[n + 1]
Lm9:
for n being Nat holds S1[n]
from NAT_1:sch 2(Lm7, Lm8);
defpred S2[ Nat] means for v being FinSequence of REAL st card (rng v) = $1 holds
ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing );
Lm10:
S2[ 0 ]
Lm11:
for n being Nat st S2[n] holds
S2[n + 1]
Lm12:
for n being Nat holds S2[n]
from NAT_1:sch 2(Lm10, Lm11);
defpred S3[ Nat] means for v1, v2 being FinSequence of REAL st len v1 = $1 & len v2 = $1 & rng v1 = rng v2 & v1 is increasing & v2 is increasing holds
v1 = v2;
Lm13:
S3[ 0 ]
Lm14:
for n being Nat st S3[n] holds
S3[n + 1]
Lm15:
for n being Nat holds S3[n]
from NAT_1:sch 2(Lm13, Lm14);
:: Theorems about the Convergence and the Limit
::