:: Chebyshev Distance
:: by Roland Coghetto
::
:: Copyright (c) 2015-2021 Association of Mizar Users

theorem Th1: :: SRINGS_5:1
for n being Nat
for x, y being Element of REAL n holds abs (x - y) = abs (y - x)
proof end;

theorem Th2: :: SRINGS_5:2
for n being Nat
for x being Element of REAL n
for i being Nat st i in Seg n holds
(abs x) . i in REAL
proof end;

theorem Th3: :: SRINGS_5:3
for x, y being Element of REAL
for xe, ye being ExtReal st x <= xe & y <= ye holds
x + y <= xe + ye
proof end;

theorem Th4: :: SRINGS_5:4
for a, c being Real
for b being R_eal st a < b & [.a,b.[ c= [.a,c.[ holds
b is Real
proof end;

theorem Th5: :: SRINGS_5:5
for n being Nat
for D being non empty set
for D1 being non empty Subset of D holds n -tuples_on D1 c= n -tuples_on D
proof end;

theorem Th6: :: SRINGS_5:6
for n being Nat
for X being non empty set
for f being Function st f = (Seg n) --> X holds
f is non-empty b1 -element FinSequence
proof end;

definition
let n be Nat;
coherence by Th6;
end;

:: deftheorem defines ProductREAL SRINGS_5:def 1 :
for n being Nat holds ProductREAL n = (Seg n) --> REAL;

theorem :: SRINGS_5:7
for n being Nat holds ProductREAL n = (Seg n) --> the carrier of R^1 ;

theorem Th7: :: SRINGS_5:8
for n being Nat holds product ((Seg n) --> REAL) = REAL n
proof end;

theorem :: SRINGS_5:9
for n being Nat holds product () = REAL n by Th7;

theorem Th8: :: SRINGS_5:10
for n being Nat
for X being set holds product ((Seg n) --> X) = n -tuples_on X
proof end;

theorem Th9: :: SRINGS_5:11
for n being Nat
for D being non empty set
for x being Tuple of n,D holds x in Funcs ((Seg n),D)
proof end;

theorem Th10: :: SRINGS_5:12
for n being Nat
for O1 being Subset of ()
for O2 being Subset of () st O1 = O2 holds
( O1 is open iff O2 is open )
proof end;

theorem :: SRINGS_5:13
for n being Nat
for p being Point of ()
for e being Point of () st e = p holds
{ (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } = { (OpenHypercube (p,(1 / m))) where m is non zero Element of NAT : verum }
proof end;

theorem Th11: :: SRINGS_5:14
for n being Nat
for r being Real
for p, q being Point of () st q in OpenHypercube (p,r) holds
p in OpenHypercube (q,r)
proof end;

theorem Th12: :: SRINGS_5:15
for n being Nat
for r being Real
for p, q being Point of () st q in OpenHypercube (p,(r / 2)) holds
OpenHypercube (q,(r / 2)) c= OpenHypercube (p,r)
proof end;

definition
let x be Element of ;
:: original: 1
redefine func x 1 -> Element of REAL ;
coherence
x 1 is Element of REAL
proof end;
:: original: 2
redefine func x 2 -> Element of REAL ;
coherence
x 2 is Element of REAL
proof end;
end;

definition
let n be Nat;
let x be Element of [:(REAL n),(REAL n):];
:: original: 1
redefine func x 1 -> Element of REAL n;
coherence
x 1 is Element of REAL n
proof end;
:: original: 2
redefine func x 2 -> Element of REAL n;
coherence
x 2 is Element of REAL n
proof end;
end;

theorem Th13: :: SRINGS_5:16
for n being Nat
for f being b1 -element FinSequence of ex x being Element of [:(REAL n),(REAL n):] st
for i being Nat st i in Seg n holds
( (x 1) . i = (f /. i) 1 & (x 2) . i = (f /. i) 2 )
proof end;

definition
let n be Nat;
coherence ;
end;

:: deftheorem defines RAT SRINGS_5:def 2 :
for n being Nat holds RAT n = n -tuples_on RAT;

theorem Th14: :: SRINGS_5:17
proof end;

registration
coherence by Th14;
end;

registration
let n be Nat;
cluster RAT n -> non empty ;
coherence
not RAT n is empty
;
end;

registration
let n be Nat;
cluster -> n -element for Element of RAT n;
coherence
for b1 being Element of RAT n holds b1 is n -element
;
end;

registration
let n be Nat;
coherence
RAT n is countable
by CARD_4:10;
end;

registration
let n be positive Nat;
correctness
coherence
not RAT n is finite
;
proof end;
end;

registration
let n be positive Nat;
coherence ;
end;

theorem Th15: :: SRINGS_5:18
for n being Nat holds RAT n is dense Subset of ()
proof end;

registration
let n be Nat;
cluster RAT n -> countable dense for Subset of ();
coherence
for b1 being Subset of () st b1 = RAT n holds
( b1 is countable & b1 is dense )
by Th15;
end;

registration
let n be Nat;
cluster countable simplex-like quasi_basis for Element of bool (bool the carrier of ());
existence
ex b1 being Basis of () st b1 is countable
by TOPGEN_4:57;
end;

registration
let n be Nat;
let e be Point of ();
coherence
proof end;
end;

definition
let n be Nat;
func OpenHypercubesRAT n -> non empty set equals :: SRINGS_5:def 3
{ () where q is Point of () : q in RAT n } ;
coherence
{ () where q is Point of () : q in RAT n } is non empty set
proof end;
end;

:: deftheorem defines OpenHypercubesRAT SRINGS_5:def 3 :
for n being Nat holds OpenHypercubesRAT n = { () where q is Point of () : q in RAT n } ;

definition
let n be Nat;
let q be Element of RAT n;
func @ q -> Point of () equals :: SRINGS_5:def 4
q;
coherence
q is Point of ()
proof end;
end;

:: deftheorem defines @ SRINGS_5:def 4 :
for n being Nat
for q being Element of RAT n holds @ q = q;

definition
let n be Nat;
let q be object ;
assume A1: q in RAT n ;
func object2RAT (q,n) -> Element of RAT n equals :Def1: :: SRINGS_5:def 5
q;
coherence
q is Element of RAT n
by A1;
end;

:: deftheorem Def1 defines object2RAT SRINGS_5:def 5 :
for n being Nat
for q being object st q in RAT n holds
object2RAT (q,n) = q;

Th16: for n being Nat holds OpenHypercubesRAT n is countable
proof end;

registration
let n be Nat;
coherence by Th16;
end;

Th17: for n being Nat holds union is countable
proof end;

registration
let n be Nat;
coherence by Th17;
end;

Th18: for n being Nat holds union is Subset-Family of ()
proof end;

theorem Th19: :: SRINGS_5:19
for n being Nat holds union is open Subset-Family of ()
proof end;

theorem Th20: :: SRINGS_5:20
for n being Nat
for O being non empty open Subset of () ex p being Element of RAT n st p in O
proof end;

theorem Th21: :: SRINGS_5:21
for n being Nat
for cB being Subset-Family of () st cB = union holds
cB is quasi_basis
proof end;

Th22: for n being Nat holds not union is empty
proof end;

registration
let n be Nat;
cluster union -> non empty ;
coherence
not union is empty
by Th22;
end;

definition
let n be Nat;
coherence by Th19;
end;

:: deftheorem defines dense_countable_OpenHypercubes SRINGS_5:def 6 :
for n being Nat holds dense_countable_OpenHypercubes n = union ;

theorem :: SRINGS_5:22
for n being Nat holds dense_countable_OpenHypercubes n = { (OpenHypercube (q,(1 / m))) where q is Point of (), m is positive Nat : q in RAT n }
proof end;

registration
let n be Nat;
cluster countable simplex-like quasi_basis for Element of bool (bool the carrier of ());
existence
ex b1 being Basis of () st b1 is countable
proof end;
end;

theorem :: SRINGS_5:23
for n being Nat holds dense_countable_OpenHypercubes n is countable Basis of () by Th21;

theorem Th23: :: SRINGS_5:24
for n being Nat
for O being open Subset of () ex Y being Subset of st
( Y is countable & O = union Y )
proof end;

theorem Th24: :: SRINGS_5:25
for n being Nat
for O being non empty open Subset of () ex Y being Subset of st
( not Y is empty & O = union Y & ex g being Function of NAT,Y st
for x being object holds
( x in O iff ex y being object st
( y in NAT & x in g . y ) ) )
proof end;

theorem Th25: :: SRINGS_5:26
for n being Nat
for O being non empty open Subset of () ex s being sequence of st
for x being object holds
( x in O iff ex y being object st
( y in NAT & x in s . y ) )
proof end;

theorem :: SRINGS_5:27
for n being Nat
for O being non empty open Subset of () ex s being sequence of st O = Union s
proof end;

definition
func the_set_of_all_left_open_real_bounded_intervals -> Subset-Family of REAL equals :: SRINGS_5:def 7
{ ].a,b.] where a, b is Real : verum } ;
coherence
{ ].a,b.] where a, b is Real : verum } is Subset-Family of REAL
proof end;
end;

:: deftheorem defines the_set_of_all_left_open_real_bounded_intervals SRINGS_5:def 7 :
the_set_of_all_left_open_real_bounded_intervals = { ].a,b.] where a, b is Real : verum } ;

registration
coherence
proof end;
end;

theorem :: SRINGS_5:28
the_set_of_all_left_open_real_bounded_intervals c= { I where I is Subset of REAL : I is left_open_interval }
proof end;

theorem :: SRINGS_5:30

definition
func the_set_of_all_right_open_real_bounded_intervals -> Subset-Family of REAL equals :: SRINGS_5:def 8
{ [.a,b.[ where a, b is Real : verum } ;
coherence
{ [.a,b.[ where a, b is Real : verum } is Subset-Family of REAL
proof end;
end;

:: deftheorem defines the_set_of_all_right_open_real_bounded_intervals SRINGS_5:def 8 :
the_set_of_all_right_open_real_bounded_intervals = { [.a,b.[ where a, b is Real : verum } ;

registration
coherence
proof end;
end;

theorem Th27: :: SRINGS_5:31
the_set_of_all_right_open_real_bounded_intervals c= { I where I is Subset of REAL : I is right_open_interval }
proof end;

Th28:
proof end;

Th29:
proof end;

Th30:
proof end;

theorem :: SRINGS_5:32

definition
let n be non zero Nat;
coherence
proof end;
end;

:: deftheorem defines ProductLeftOpenIntervals SRINGS_5:def 9 :
for n being non zero Nat holds ProductLeftOpenIntervals n = (Seg n) --> the_set_of_all_left_open_real_bounded_intervals;

theorem :: SRINGS_5:33
for n being non zero Nat holds ProductLeftOpenIntervals n = (Seg n) --> { ].a,b.] where a, b is Real : verum } ;

theorem Th30: :: SRINGS_5:34
for n being non zero Nat holds MeasurableRectangle is Semiring of (REAL n)
proof end;

theorem :: SRINGS_5:35
for n being non zero Nat
for x being object st x in MeasurableRectangle holds
ex y being Subset of (REAL n) st
( x = y & ( for i being Nat st i in Seg n holds
ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in ].a,b.] ) )
proof end;

theorem Th31: :: SRINGS_5:36
for n being non zero Nat
for x being object st x in MeasurableRectangle holds
ex y being Subset of (REAL n) ex f being b1 -element FinSequence of st
( x = y & ( for t being Element of REAL n holds
( t in y iff for i being Nat st i in Seg n holds
t . i in ].((f /. i) 1),((f /. i) 2).] ) ) )
proof end;

theorem Th32: :: SRINGS_5:37
for n being non zero Nat
for x being object st x in MeasurableRectangle holds
ex y being Subset of (REAL n) ex a, b being Element of REAL n st
( x = y & ( for s being object holds
( s in y iff ex t being Element of REAL n st
( s = t & ( for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ) ) ) ) )
proof end;

theorem :: SRINGS_5:38
for n being non zero Nat
for x being set st x in MeasurableRectangle holds
ex a, b being Element of REAL n st
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] )
proof end;

definition
let n be non zero Nat;
coherence
proof end;
end;

:: deftheorem defines ProductRightOpenIntervals SRINGS_5:def 10 :
for n being non zero Nat holds ProductRightOpenIntervals n = (Seg n) --> the_set_of_all_right_open_real_bounded_intervals;

theorem :: SRINGS_5:39
for n being non zero Nat holds ProductRightOpenIntervals n = (Seg n) --> { [.a,b.[ where a, b is Real : verum } ;

theorem Th33: :: SRINGS_5:40
for n being non zero Nat holds MeasurableRectangle is Semiring of (REAL n)
proof end;

theorem :: SRINGS_5:41
for n being non zero Nat
for x being object st x in MeasurableRectangle holds
ex y being Subset of (REAL n) st
( x = y & ( for i being Nat st i in Seg n holds
ex a, b being Real st
for t being Element of REAL n st t in y holds
t . i in [.a,b.[ ) )
proof end;

theorem Th34: :: SRINGS_5:42
for n being non zero Nat
for x being object st x in MeasurableRectangle holds
ex y being Subset of (REAL n) ex f being b1 -element FinSequence of st
( x = y & ( for t being Element of REAL n holds
( t in y iff for i being Nat st i in Seg n holds
t . i in [.((f /. i) 1),((f /. i) 2).[ ) ) )
proof end;

theorem Th35: :: SRINGS_5:43
for n being non zero Nat
for x being object st x in MeasurableRectangle holds
ex y being Subset of (REAL n) ex a, b being Element of REAL n st
( x = y & ( for s being object holds
( s in y iff ex t being Element of REAL n st
( s = t & ( for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ) ) ) ) )
proof end;

theorem :: SRINGS_5:44
for n being non zero Nat
for x being set st x in MeasurableRectangle holds
ex a, b being Element of REAL n st
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ )
proof end;

definition
let n be Nat;
let X be set ;
func Product (n,X) -> set means :Def2: :: SRINGS_5:def 11
for f being object holds
( f in it iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) );
existence
ex b1 being set st
for f being object holds
( f in b1 iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) )
proof end;
uniqueness
for b1, b2 being set st ( for f being object holds
( f in b1 iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) ) ) & ( for f being object holds
( f in b2 iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Product SRINGS_5:def 11 :
for n being Nat
for X, b3 being set holds
( b3 = Product (n,X) iff for f being object holds
( f in b3 iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) ) );

theorem Th36: :: SRINGS_5:45
for n being Nat
for X being set holds Product (n,X) c= bool (Funcs ((dom ((Seg n) --> X)),(union (Union ((Seg n) --> X)))))
proof end;

theorem Th37: :: SRINGS_5:46
for n being Nat
for X being set
for S being Subset-Family of X holds Product (n,S) is Subset-Family of (product ((Seg n) --> X))
proof end;

theorem Th38: :: SRINGS_5:47
for n being Nat
for X being set
for S being non empty Subset-Family of X holds Product (n,S) = { () where f is Tuple of n,S : verum }
proof end;

theorem Th39: :: SRINGS_5:48
for X being set
for n being non zero Nat holds Product (n,X) c= bool (Funcs ((Seg n),()))
proof end;

theorem Th40: :: SRINGS_5:49
for n being non zero Nat
for X being non empty set
for S being non empty Subset-Family of X st S <> holds
Product (n,S) c= bool (Funcs ((Seg n),X))
proof end;

theorem :: SRINGS_5:50
for n being non zero Nat
for X being non empty set
for S being non empty Subset-Family of X st S <> holds
union (Product (n,S)) c= Funcs ((Seg n),X)
proof end;

registration
let n be Nat;
let X be non empty set ;
cluster Product (n,X) -> non empty ;
coherence
not Product (n,X) is empty
proof end;
end;

Lm1: for n being Nat
for X being non empty set
for S being non empty Subset-Family of X
for x being Element of Product (n,S) ex s being Tuple of n,S st
for t being Element of Funcs ((Seg n),X) holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x )

proof end;

Lm2: for n being Nat
for X being non empty set
for S being non empty Subset-Family of X
for x being Subset of (Funcs ((Seg n),X))
for s being Tuple of n,S st ( for t being Element of Funcs ((Seg n),X) holds
( t in x iff for i being Nat st i in Seg n holds
t . i in s . i ) ) holds
x is Element of Product (n,S)

proof end;

theorem :: SRINGS_5:51
for n being Nat
for X being non empty set
for S being non empty Subset-Family of X
for x being Subset of (Funcs ((Seg n),X)) holds
( x is Element of Product (n,S) iff ex s being Tuple of n,S st
for t being Element of Funcs ((Seg n),X) holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x ) ) by ;

definition
func the_set_of_all_closed_real_bounded_intervals -> Subset-Family of REAL equals :: SRINGS_5:def 12
{ [.a,b.] where a, b is Real : verum } ;
coherence
{ [.a,b.] where a, b is Real : verum } is Subset-Family of REAL
proof end;
end;

:: deftheorem defines the_set_of_all_closed_real_bounded_intervals SRINGS_5:def 12 :
the_set_of_all_closed_real_bounded_intervals = { [.a,b.] where a, b is Real : verum } ;

theorem :: SRINGS_5:52
the_set_of_all_closed_real_bounded_intervals = { I where I is Subset of REAL : I is closed_interval }
proof end;

registration
coherence
proof end;
end;

registration end;

theorem :: SRINGS_5:53
for n being Nat holds (Seg n) --> the_set_of_all_closed_real_bounded_intervals is b1 -element FinSequence
proof end;

definition
func the_set_of_all_open_real_bounded_intervals -> Subset-Family of REAL equals :: SRINGS_5:def 13
{ ].a,b.[ where a, b is Real : verum } ;
coherence
{ ].a,b.[ where a, b is Real : verum } is Subset-Family of REAL
proof end;
end;

:: deftheorem defines the_set_of_all_open_real_bounded_intervals SRINGS_5:def 13 :
the_set_of_all_open_real_bounded_intervals = { ].a,b.[ where a, b is Real : verum } ;

theorem :: SRINGS_5:54
the_set_of_all_open_real_bounded_intervals c= { I where I is Subset of REAL : I is open_interval }
proof end;

registration
coherence
proof end;
end;

registration end;

theorem :: SRINGS_5:55
for n being Nat holds (Seg n) --> the_set_of_all_open_real_bounded_intervals is b1 -element FinSequence
proof end;

theorem Th41: :: SRINGS_5:56
for n being Nat
for S being Subset-Family of REAL holds Product (n,S) is Subset-Family of (REAL n)
proof end;

definition
let n be Nat;
let S be Subset-Family of REAL;
:: original: Product
redefine func Product (n,S) -> Subset-Family of (REAL n);
coherence
Product (n,S) is Subset-Family of (REAL n)
by Th41;
end;

theorem Th42: :: SRINGS_5:57
for n being Nat
for S being non empty Subset-Family of REAL
for x being Subset of (REAL n) holds
( x is Element of Product (n,S) iff ex s being Tuple of n,S st
for t being Element of REAL n holds
( ( for i being Nat st i in Seg n holds
t . i in s . i ) iff t in x ) )
proof end;

theorem Th43: :: SRINGS_5:58
for n being non zero Nat
for s being Tuple of n, the_set_of_all_closed_real_bounded_intervals ex a, b being Element of REAL n st
for i being Nat st i in Seg n holds
s . i = [.(a . i),(b . i).]
proof end;

theorem :: SRINGS_5:59
for n being non zero Nat
for x being Element of Product (n,the_set_of_all_closed_real_bounded_intervals) ex a, b being Element of REAL n st
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).] )
proof end;

theorem :: SRINGS_5:60
for n being non zero Nat
for x being Subset of (REAL n)
for a, b being Element of REAL n st ( for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).] ) ) holds
x is Element of Product (n,the_set_of_all_closed_real_bounded_intervals)
proof end;

theorem Th44: :: SRINGS_5:61
for n being non zero Nat
for x being Subset of (REAL n)
for a, b being Element of REAL n st ( for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] ) ) holds
x is Element of Product (n,the_set_of_all_left_open_real_bounded_intervals)
proof end;

theorem Th45: :: SRINGS_5:62
for n being non zero Nat
for x being Subset of (REAL n)
for a, b being Element of REAL n st ( for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ ) ) holds
x is Element of Product (n,the_set_of_all_right_open_real_bounded_intervals)
proof end;

theorem Th46: :: SRINGS_5:63
for n being non zero Nat
for s being Tuple of n, the_set_of_all_left_open_real_bounded_intervals ex a, b being Element of REAL n st
for i being Nat st i in Seg n holds
s . i = ].(a . i),(b . i).]
proof end;

theorem :: SRINGS_5:64
for n being non zero Nat
for x being Element of Product (n,the_set_of_all_left_open_real_bounded_intervals) ex a, b being Element of REAL n st
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] )
proof end;

theorem Th47: :: SRINGS_5:65
for n being non zero Nat
for s being Tuple of n, the_set_of_all_right_open_real_bounded_intervals ex a, b being Element of REAL n st
for i being Nat st i in Seg n holds
s . i = [.(a . i),(b . i).[
proof end;

theorem :: SRINGS_5:66
for n being non zero Nat
for x being Element of Product (n,the_set_of_all_right_open_real_bounded_intervals) ex a, b being Element of REAL n st
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ )
proof end;

definition
let n be Nat;
let a, b be Element of REAL n;
func ClosedHyperInterval (a,b) -> Subset of (REAL n) means :Def3: :: SRINGS_5:def 14
for x being object holds
( x in it iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).] ) ) );
existence
ex b1 being Subset of (REAL n) st
for x being object holds
( x in b1 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).] ) ) )
proof end;
uniqueness
for b1, b2 being Subset of (REAL n) st ( for x being object holds
( x in b1 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).] ) ) ) ) & ( for x being object holds
( x in b2 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).] ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines ClosedHyperInterval SRINGS_5:def 14 :
for n being Nat
for a, b being Element of REAL n
for b4 being Subset of (REAL n) holds
( b4 = ClosedHyperInterval (a,b) iff for x being object holds
( x in b4 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).] ) ) ) );

definition
let n be Nat;
let a, b be Element of REAL n;
func OpenHyperInterval (a,b) -> Subset of (REAL n) means :Def4: :: SRINGS_5:def 15
for x being object holds
( x in it iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).[ ) ) );
existence
ex b1 being Subset of (REAL n) st
for x being object holds
( x in b1 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).[ ) ) )
proof end;
uniqueness
for b1, b2 being Subset of (REAL n) st ( for x being object holds
( x in b1 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).[ ) ) ) ) & ( for x being object holds
( x in b2 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).[ ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines OpenHyperInterval SRINGS_5:def 15 :
for n being Nat
for a, b being Element of REAL n
for b4 being Subset of (REAL n) holds
( b4 = OpenHyperInterval (a,b) iff for x being object holds
( x in b4 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).[ ) ) ) );

definition
let n be Nat;
let a, b be Element of REAL n;
func LeftOpenHyperInterval (a,b) -> Subset of (REAL n) means :Def5: :: SRINGS_5:def 16
for x being object holds
( x in it iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).] ) ) );
existence
ex b1 being Subset of (REAL n) st
for x being object holds
( x in b1 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).] ) ) )
proof end;
uniqueness
for b1, b2 being Subset of (REAL n) st ( for x being object holds
( x in b1 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).] ) ) ) ) & ( for x being object holds
( x in b2 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).] ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines LeftOpenHyperInterval SRINGS_5:def 16 :
for n being Nat
for a, b being Element of REAL n
for b4 being Subset of (REAL n) holds
( b4 = LeftOpenHyperInterval (a,b) iff for x being object holds
( x in b4 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in ].(a . i),(b . i).] ) ) ) );

definition
let n be Nat;
let a, b be Element of REAL n;
func RightOpenHyperInterval (a,b) -> Subset of (REAL n) means :Def6: :: SRINGS_5:def 17
for x being object holds
( x in it iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).[ ) ) );
existence
ex b1 being Subset of (REAL n) st
for x being object holds
( x in b1 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).[ ) ) )
proof end;
uniqueness
for b1, b2 being Subset of (REAL n) st ( for x being object holds
( x in b1 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).[ ) ) ) ) & ( for x being object holds
( x in b2 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).[ ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines RightOpenHyperInterval SRINGS_5:def 17 :
for n being Nat
for a, b being Element of REAL n
for b4 being Subset of (REAL n) holds
( b4 = RightOpenHyperInterval (a,b) iff for x being object holds
( x in b4 iff ex y being Element of REAL n st
( x = y & ( for i being Nat st i in Seg n holds
y . i in [.(a . i),(b . i).[ ) ) ) );

theorem Th48: :: SRINGS_5:67
for n being Nat
for a being Element of REAL n holds ClosedHyperInterval (a,a) = {a}
proof end;

registration
let n be Nat;
let a be Element of REAL n;
coherence
ClosedHyperInterval (a,a) is trivial
proof end;
end;

theorem :: SRINGS_5:68
for n being Nat
for a, b being Element of REAL n holds
( OpenHyperInterval (a,b) c= LeftOpenHyperInterval (a,b) & OpenHyperInterval (a,b) c= RightOpenHyperInterval (a,b) & LeftOpenHyperInterval (a,b) c= ClosedHyperInterval (a,b) & RightOpenHyperInterval (a,b) c= ClosedHyperInterval (a,b) )
proof end;

definition
let n be Nat;
let a, b be Element of REAL n;
pred a <= b means :: SRINGS_5:def 18
for i being Nat st i in Seg n holds
a . i <= b . i;
reflexivity
for a being Element of REAL n
for i being Nat st i in Seg n holds
a . i <= a . i
;
end;

:: deftheorem defines <= SRINGS_5:def 18 :
for n being Nat
for a, b being Element of REAL n holds
( a <= b iff for i being Nat st i in Seg n holds
a . i <= b . i );

theorem :: SRINGS_5:69
for n being Nat
for a, b, c being Element of REAL n st a <= b & b <= c holds
a <= c
proof end;

theorem Th49: :: SRINGS_5:70
for n being Nat
for a, b, c, d being Element of REAL n st a <= c & d <= b holds
ClosedHyperInterval (c,d) c= ClosedHyperInterval (a,b)
proof end;

theorem :: SRINGS_5:71
for n being Nat
for a, b being Element of REAL n st a <= b holds
not ClosedHyperInterval (a,b) is empty
proof end;

definition
let n be Nat;
let a, b be Element of REAL n;
pred a < b means :: SRINGS_5:def 19
for i being Nat st i in Seg n holds
a . i < b . i;
end;

:: deftheorem defines < SRINGS_5:def 19 :
for n being Nat
for a, b being Element of REAL n holds
( a < b iff for i being Nat st i in Seg n holds
a . i < b . i );

theorem :: SRINGS_5:72
for n being Nat
for a, b, c being Element of REAL n st a < b & b < c holds
a < c
proof end;

theorem :: SRINGS_5:73
for n being Nat
for a, b being Element of REAL n st b < a & not n is zero holds
ClosedHyperInterval (a,b) is empty
proof end;

theorem Th50: :: SRINGS_5:74
for r being Real
for n being Nat holds n |-> r is Element of REAL n
proof end;

definition
let n be Nat;
let r be Real;
:: original: |->
redefine func n |-> r -> Element of REAL n;
coherence
n |-> r is Element of REAL n
by Th50;
end;

definition
let r be Real;
:: original: <*
redefine func <*r*> -> Element of REAL 1;
coherence
<*r*> is Element of REAL 1
proof end;
end;

theorem Th51: :: SRINGS_5:75
for r being Real
for n being non zero Nat
for e being Point of () ex a being Element of REAL n st
( a = e & OpenHypercube (e,r) = OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))) )
proof end;

theorem Th52: :: SRINGS_5:76
for n being Nat
for b being Element of REAL n
for p being Point of () ex a being Element of REAL n st
( a = p & ClosedHypercube (p,b) = ClosedHyperInterval ((a - b),(a + b)) )
proof end;

theorem :: SRINGS_5:77
for r, s, x being Real holds
( x in [.r,s.] iff 1 |-> x in ClosedHyperInterval (<*r*>,<*s*>) )
proof end;

theorem :: SRINGS_5:78
for r, s, x being Real holds
( x in ].r,s.[ iff 1 |-> x in OpenHyperInterval (<*r*>,<*s*>) )
proof end;

theorem :: SRINGS_5:79
for r, s, x being Real holds
( x in ].r,s.] iff 1 |-> x in LeftOpenHyperInterval (<*r*>,<*s*>) )
proof end;

theorem :: SRINGS_5:80
for r, s, x being Real holds
( x in [.r,s.[ iff 1 |-> x in RightOpenHyperInterval (<*r*>,<*s*>) )
proof end;

theorem Th53: :: SRINGS_5:81
for n being non zero Nat
for s being Tuple of n, the_set_of_all_open_real_bounded_intervals ex a, b being Element of REAL n st
for i being Nat st i in Seg n holds
s . i = ].(a . i),(b . i).[
proof end;

theorem :: SRINGS_5:82
for n being non zero Nat
for x being Element of Product (n,the_set_of_all_open_real_bounded_intervals) ex a, b being Element of REAL n st
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).[ )
proof end;

theorem Th54: :: SRINGS_5:83
for n being non zero Nat
for s being Tuple of n, the_set_of_all_left_open_real_bounded_intervals ex a, b being Element of REAL n st
for i being Nat st i in Seg n holds
s . i = ].(a . i),(b . i).]
proof end;

theorem :: SRINGS_5:84
for n being non zero Nat
for x being Element of Product (n,the_set_of_all_left_open_real_bounded_intervals) ex a, b being Element of REAL n st
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in ].(a . i),(b . i).] )
proof end;

theorem Th55: :: SRINGS_5:85
for n being non zero Nat
for s being Tuple of n, the_set_of_all_right_open_real_bounded_intervals ex a, b being Element of REAL n st
for i being Nat st i in Seg n holds
s . i = [.(a . i),(b . i).[
proof end;

theorem :: SRINGS_5:86
for n being non zero Nat
for x being Element of Product (n,the_set_of_all_right_open_real_bounded_intervals) ex a, b being Element of REAL n st
for t being Element of REAL n holds
( t in x iff for i being Nat st i in Seg n holds
t . i in [.(a . i),(b . i).[ )
proof end;

theorem :: SRINGS_5:87
for n being non zero Nat holds MeasurableRectangle = Product (n,the_set_of_all_left_open_real_bounded_intervals)
proof end;

theorem :: SRINGS_5:88
for n being non zero Nat holds MeasurableRectangle = Product (n,the_set_of_all_right_open_real_bounded_intervals)
proof end;

definition
let n be non zero Nat;
func Infty_dist n -> Function of [:(REAL n),(REAL n):],REAL means :Def7: :: SRINGS_5:def 20
for x, y being Element of REAL n holds it . (x,y) = sup (rng (abs (x - y)));
existence
ex b1 being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds b1 . (x,y) = sup (rng (abs (x - y)))
proof end;
uniqueness
for b1, b2 being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b1 . (x,y) = sup (rng (abs (x - y))) ) & ( for x, y being Element of REAL n holds b2 . (x,y) = sup (rng (abs (x - y))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines Infty_dist SRINGS_5:def 20 :
for n being non zero Nat
for b2 being Function of [:(REAL n),(REAL n):],REAL holds
( b2 = Infty_dist n iff for x, y being Element of REAL n holds b2 . (x,y) = sup (rng (abs (x - y))) );

theorem Th56: :: SRINGS_5:89
for n being non zero Nat
for x, y being Element of REAL n holds
( { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } is real-membered & { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } = rng (abs (x - y)) )
proof end;

theorem Th57: :: SRINGS_5:90
for n being non zero Nat
for x, y being Element of REAL n ex S being ext-real-membered set st
( S = { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } & () . (x,y) = sup S )
proof end;

theorem Th58: :: SRINGS_5:91
for n being non zero Nat
for x, y being Element of REAL n holds () . (x,y) = (abs (x - y)) . (max_diff_index (x,y))
proof end;

theorem Th59: :: SRINGS_5:92
for n being non zero Nat
for x, y being Element of REAL n holds
( () . (x,y) = 0 iff x = y )
proof end;

theorem Th60: :: SRINGS_5:93
for n being non zero Nat
for x, y being Element of REAL n holds () . (x,y) = () . (y,x)
proof end;

theorem Th61: :: SRINGS_5:94
for n being non zero Nat
for x, y, z being Element of REAL n holds () . (x,y) <= (() . (x,z)) + (() . (z,y))
proof end;

theorem Th62: :: SRINGS_5:95
for n being non zero Nat holds Infty_dist n is_metric_of REAL n
proof end;

theorem Th63: :: SRINGS_5:96
() . (,|[1,1]|) = sqrt 2
proof end;

theorem Th64: :: SRINGS_5:97
() . (,|[1,1]|) = 1
proof end;

theorem Th65: :: SRINGS_5:98
for x, y being Element of REAL 1 holds () . (x,y) = |.((x . 1) - (y . 1)).|
proof end;

theorem Th66: :: SRINGS_5:99
for x, y being Element of REAL 1 holds () . (x,y) = |.((x . 1) - (y . 1)).|
proof end;

theorem :: SRINGS_5:100
proof end;

theorem :: SRINGS_5:101
proof end;

definition
let n be non zero Nat;
func EMINFTY n -> strict MetrSpace equals :: SRINGS_5:def 21
MetrStruct(# (REAL n),() #);
coherence
MetrStruct(# (REAL n),() #) is strict MetrSpace
proof end;
end;

:: deftheorem defines EMINFTY SRINGS_5:def 21 :
for n being non zero Nat holds EMINFTY n = MetrStruct(# (REAL n),() #);

registration
let n be non zero Nat;
cluster EMINFTY n -> non empty strict ;
coherence
not EMINFTY n is empty
;
end;

definition
let n be non zero Nat;
func TOP-REAL-INFTY n -> strict RLTopStruct means :Def8: :: SRINGS_5:def 22
( TopStruct(# the carrier of it, the topology of it #) = TopSpaceMetr () & RLSStruct(# the carrier of it, the ZeroF of it, the addF of it, the Mult of it #) = RealVectSpace (Seg n) );
existence
ex b1 being strict RLTopStruct st
( TopStruct(# the carrier of b1, the topology of b1 #) = TopSpaceMetr () & RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = RealVectSpace (Seg n) )
proof end;
uniqueness
for b1, b2 being strict RLTopStruct st TopStruct(# the carrier of b1, the topology of b1 #) = TopSpaceMetr () & RLSStruct(# the carrier of b1, the ZeroF of b1, the addF of b1, the Mult of b1 #) = RealVectSpace (Seg n) & TopStruct(# the carrier of b2, the topology of b2 #) = TopSpaceMetr () & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = RealVectSpace (Seg n) holds
b1 = b2
;
end;

:: deftheorem Def8 defines TOP-REAL-INFTY SRINGS_5:def 22 :
for n being non zero Nat
for b2 being strict RLTopStruct holds
( b2 = TOP-REAL-INFTY n iff ( TopStruct(# the carrier of b2, the topology of b2 #) = TopSpaceMetr () & RLSStruct(# the carrier of b2, the ZeroF of b2, the addF of b2, the Mult of b2 #) = RealVectSpace (Seg n) ) );

theorem :: SRINGS_5:102
for n being non zero Nat holds RLSStruct(# the carrier of (), the ZeroF of (), the addF of (), the Mult of () #) = RLSStruct(# the carrier of (), the ZeroF of (), the addF of (), the Mult of () #)
proof end;

registration
let n be non zero Nat;
coherence
not TOP-REAL-INFTY n is empty
proof end;
end;

theorem :: SRINGS_5:103
for r being Real
for x being Element of REAL 0 holds
( Intervals (x,r) is empty & product (Intervals (x,r)) = ) by CARD_3:10;

theorem Th67: :: SRINGS_5:104
for r being Real
for n being non zero Nat
for x being Element of REAL n st r <= 0 holds
product (Intervals (x,r)) is empty
proof end;

definition
let n be non zero Nat;
let p be Element of ();
func @ p -> Element of REAL n equals :: SRINGS_5:def 23
p;
coherence
p is Element of REAL n
;
end;

:: deftheorem defines @ SRINGS_5:def 23 :
for n being non zero Nat
for p being Element of () holds @ p = p;

theorem Th68: :: SRINGS_5:105
for r being Real
for n being non zero Nat
for p being Element of () holds Ball (p,r) = product (Intervals ((@ p),r))
proof end;

theorem :: SRINGS_5:106
for r being Real
for n being non zero Nat
for p being Element of ()
for e being Point of () st e = p holds
Ball (p,r) = OpenHypercube (e,r)
proof end;

registration
let n be non zero Nat;
let p be Element of ();
let r be negative Real;
cluster cl_Ball (p,r) -> empty ;
coherence
cl_Ball (p,r) is empty
proof end;
end;

theorem Th69: :: SRINGS_5:107
for r being Real
for n being non zero Nat
for p being Element of ()
for t being object holds
( t in cl_Ball (p,r) iff ex f being Function st
( t = f & dom f = Seg n & ( for i being Nat st i in Seg n holds
f . i in [.(((@ p) . i) - r),(((@ p) . i) + r).] ) ) )
proof end;

theorem Th70: :: SRINGS_5:108
for r being Real
for n being non zero Nat
for p being Point of ()
for q being Element of () st q = p holds
cl_Ball (q,r) = ClosedHypercube (p,(n |-> r))
proof end;

theorem :: SRINGS_5:109
for r being Real
for n being non zero Nat
for p being Element of () holds Ball (p,r) = OpenHyperInterval (((@ p) - (n |-> r)),((@ p) + (n |-> r)))
proof end;

theorem :: SRINGS_5:110
for r being Real
for n being non zero Nat
for p being Element of () holds cl_Ball (p,r) = ClosedHyperInterval (((@ p) - (n |-> r)),((@ p) + (n |-> r)))
proof end;