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
::