:: Chebyshev Distance
:: by Roland Coghetto
::
:: Received December 31, 2015
:: 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 b₁ -element FinSequence

proof end;

definition

let n be Nat;

func ProductREAL n -> non-empty n -element FinSequence equals :: SRINGS_5:def 1
(Seg n) --> REAL;

coherence
(Seg n) --> REAL is non-empty n -element FinSequence 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 (ProductREAL n) = 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 (TOP-REAL n)
for O2 being Subset of (TopSpaceMetr (Euclid n)) 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 (TOP-REAL n)
for e being Point of (Euclid n) 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 (TOP-REAL n) 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 (TOP-REAL n) st q in OpenHypercube (p,(r / 2)) holds
OpenHypercube (q,(r / 2)) c= OpenHypercube (p,r)

proof end;

definition

let x be Element of [:REAL,REAL:];
:: 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 b₁ -element FinSequence of [:REAL,REAL:] 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;

func RAT n -> FinSequenceSet of RAT equals :: SRINGS_5:def 2
n -tuples_on RAT;

coherence
n -tuples_on RAT is FinSequenceSet of RAT ;

end;

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

theorem Th14: :: SRINGS_5:17

RAT 0 = {0}

proof end;

registration

cluster RAT 0 -> trivial ;

coherence
RAT 0 is trivial 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 b₁ being Element of RAT n holds b₁ is n -element ;

end;

registration

let n be Nat;

cluster RAT n -> countable ;

coherence
RAT n is countable by CARD_4:10;

end;

registration

let n be positive Nat;

cluster RAT n -> infinite ;

correctness
coherence
not RAT n is finite ;

proof end;

end;

registration

let n be positive Nat;

cluster RAT n -> denumerable ;

coherence
RAT n is denumerable ;

end;

theorem Th15: :: SRINGS_5:18

for n being Nat holds RAT n is dense Subset of (TOP-REAL n)

proof end;

registration

let n be Nat;

cluster RAT n -> countable dense for Subset of (TOP-REAL n);

coherence
for b₁ being Subset of (TOP-REAL n) st b₁ = RAT n holds
( b₁ is countable & b₁ is dense ) by Th15;

end;

registration

let n be Nat;

cluster countable simplex-like quasi_basis for Element of bool (bool the carrier of (TOP-REAL n));

existence
ex b₁ being Basis of (TOP-REAL n) st b₁ is countable by TOPGEN_4:57;

end;

registration

let n be Nat;
let e be Point of (Euclid n);

cluster OpenHypercubes e -> countable ;

coherence
OpenHypercubes e is countable

proof end;

end;

definition

let n be Nat;

func OpenHypercubesRAT n -> non empty set equals :: SRINGS_5:def 3
{ (OpenHypercubes q) where q is Point of (Euclid n) : q in RAT n } ;

coherence
{ (OpenHypercubes q) where q is Point of (Euclid n) : 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 = { (OpenHypercubes q) where q is Point of (Euclid n) : q in RAT n } ;

definition

let n be Nat;
let q be Element of RAT n;

func @ q -> Point of (Euclid n) equals :: SRINGS_5:def 4
q;

coherence
q is Point of (Euclid n)

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;

cluster OpenHypercubesRAT n -> non empty countable ;

coherence
OpenHypercubesRAT n is countable by Th16;

end;

Th17: for n being Nat holds union (OpenHypercubesRAT n) is countable

proof end;

registration

let n be Nat;

cluster union (OpenHypercubesRAT n) -> countable ;

coherence
union (OpenHypercubesRAT n) is countable by Th17;

end;

Th18: for n being Nat holds union (OpenHypercubesRAT n) is Subset-Family of (TOP-REAL n)

proof end;

theorem Th19: :: SRINGS_5:19

for n being Nat holds union (OpenHypercubesRAT n) is open Subset-Family of (TOP-REAL n)

proof end;

theorem Th20: :: SRINGS_5:20

for n being Nat
for O being non empty open Subset of (TOP-REAL n) 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 (TOP-REAL n) st cB = union (OpenHypercubesRAT n) holds
cB is quasi_basis

proof end;

Th22: for n being Nat holds not union (OpenHypercubesRAT n) is empty

proof end;

registration

let n be Nat;

cluster union (OpenHypercubesRAT n) -> non empty ;

coherence
not union (OpenHypercubesRAT n) is empty by Th22;

end;

definition

let n be Nat;

func dense_countable_OpenHypercubes n -> countable open Subset-Family of (TOP-REAL n) equals :: SRINGS_5:def 6
union (OpenHypercubesRAT n);

coherence
union (OpenHypercubesRAT n) is countable open Subset-Family of (TOP-REAL n) by Th19;

end;

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

theorem :: SRINGS_5:22

for n being Nat holds dense_countable_OpenHypercubes n = { (OpenHypercube (q,(1 / m))) where q is Point of (Euclid n), 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 (TOP-REAL n));

existence
ex b₁ being Basis of (TOP-REAL n) st b₁ is countable

proof end;

end;

theorem :: SRINGS_5:23

for n being Nat holds dense_countable_OpenHypercubes n is countable Basis of (TOP-REAL n) by Th21;

theorem Th23: :: SRINGS_5:24

for n being Nat
for O being open Subset of (TOP-REAL n) ex Y being Subset of (dense_countable_OpenHypercubes n) 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 (TOP-REAL n) ex Y being Subset of (dense_countable_OpenHypercubes n) 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 (TOP-REAL n) ex s being sequence of (dense_countable_OpenHypercubes n) 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 (TOP-REAL n) ex s being sequence of (dense_countable_OpenHypercubes n) 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

cluster the_set_of_all_left_open_real_bounded_intervals -> non empty ;

coherence
not the_set_of_all_left_open_real_bounded_intervals is empty

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 Th26: :: SRINGS_5:29

( the_set_of_all_left_open_real_bounded_intervals is cap-closed & the_set_of_all_left_open_real_bounded_intervals is diff-finite-partition-closed & the_set_of_all_left_open_real_bounded_intervals is with_empty_element & the_set_of_all_left_open_real_bounded_intervals is with_countable_Cover )

proof end;

theorem :: SRINGS_5:30

the_set_of_all_left_open_real_bounded_intervals is Semiring of REAL by Th26, SRINGS_3:10;

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

cluster the_set_of_all_right_open_real_bounded_intervals -> non empty ;

coherence
not the_set_of_all_right_open_real_bounded_intervals is empty

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: the_set_of_all_right_open_real_bounded_intervals is with_empty_element

proof end;

Th29: ( the_set_of_all_right_open_real_bounded_intervals is cap-closed & the_set_of_all_right_open_real_bounded_intervals is diff-finite-partition-closed & the_set_of_all_right_open_real_bounded_intervals is with_empty_element )

proof end;

Th30: the_set_of_all_right_open_real_bounded_intervals is with_countable_Cover

proof end;

registration

cluster the_set_of_all_right_open_real_bounded_intervals -> with_empty_element diff-finite-partition-closed with_countable_Cover cap-closed ;

coherence
( the_set_of_all_right_open_real_bounded_intervals is cap-closed & the_set_of_all_right_open_real_bounded_intervals is diff-finite-partition-closed & the_set_of_all_right_open_real_bounded_intervals is with_empty_element & the_set_of_all_right_open_real_bounded_intervals is with_countable_Cover ) by Th29, Th30;

end;

theorem :: SRINGS_5:32

the_set_of_all_right_open_real_bounded_intervals is Semiring of REAL by SRINGS_3:10;

definition

let n be non zero Nat;

func ProductLeftOpenIntervals n -> ClassicalSemiringFamily of ProductREAL n equals :: SRINGS_5:def 9
(Seg n) --> the_set_of_all_left_open_real_bounded_intervals;

coherence
(Seg n) --> the_set_of_all_left_open_real_bounded_intervals is ClassicalSemiringFamily of ProductREAL n

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 (ProductLeftOpenIntervals n) 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 (ProductLeftOpenIntervals n) 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 (ProductLeftOpenIntervals n) holds
ex y being Subset of (REAL n) ex f being b₁ -element FinSequence of [:REAL,REAL:] 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 (ProductLeftOpenIntervals n) 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 (ProductLeftOpenIntervals n) 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;

func ProductRightOpenIntervals n -> ClassicalSemiringFamily of ProductREAL n equals :: SRINGS_5:def 10
(Seg n) --> the_set_of_all_right_open_real_bounded_intervals;

coherence
(Seg n) --> the_set_of_all_right_open_real_bounded_intervals is ClassicalSemiringFamily of ProductREAL n

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 (ProductRightOpenIntervals n) 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 (ProductRightOpenIntervals n) 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 (ProductRightOpenIntervals n) holds
ex y being Subset of (REAL n) ex f being b₁ -element FinSequence of [:REAL,REAL:] 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 (ProductRightOpenIntervals n) 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 (ProductRightOpenIntervals n) 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 b₁ being set st
for f being object holds
( f in b₁ iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for f being object holds
( f in b₁ iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) ) ) & ( for f being object holds
( f in b₂ iff ex g being Function st
( f = product g & g in product ((Seg n) --> X) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Product SRINGS_5:def 11 :
for n being Nat
for X, b₃ being set holds
( b₃ = Product (n,X) iff for f being object holds
( f in b₃ 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) = { (product f) 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),(union X)))

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 Lm1, Lm2;

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

cluster the_set_of_all_closed_real_bounded_intervals -> non empty ;

coherence
not the_set_of_all_closed_real_bounded_intervals is empty

proof end;

end;

registration

cluster the_set_of_all_closed_real_bounded_intervals -> with_empty_element with_countable_Cover cap-closed ;

coherence
( the_set_of_all_closed_real_bounded_intervals is cap-closed & the_set_of_all_closed_real_bounded_intervals is with_empty_element & the_set_of_all_closed_real_bounded_intervals is with_countable_Cover )

proof end;

end;

theorem :: SRINGS_5:53

for n being Nat holds (Seg n) --> the_set_of_all_closed_real_bounded_intervals is b₁ -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

cluster the_set_of_all_open_real_bounded_intervals -> non empty ;

coherence
not the_set_of_all_open_real_bounded_intervals is empty

proof end;

end;

registration

cluster the_set_of_all_open_real_bounded_intervals -> with_empty_element with_countable_Cover cap-closed ;

coherence
( the_set_of_all_open_real_bounded_intervals is cap-closed & the_set_of_all_open_real_bounded_intervals is with_empty_element & the_set_of_all_open_real_bounded_intervals is with_countable_Cover )

proof end;

end;

theorem :: SRINGS_5:55

for n being Nat holds (Seg n) --> the_set_of_all_open_real_bounded_intervals is b₁ -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 b₁ being Subset of (REAL n) st
for x being object holds
( x in b₁ 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 b₁, b₂ being Subset of (REAL n) st ( for x being object holds
( x in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines ClosedHyperInterval SRINGS_5:def 14 :
for n being Nat
for a, b being Element of REAL n
for b₄ being Subset of (REAL n) holds
( b₄ = ClosedHyperInterval (a,b) iff for x being object holds
( x in b₄ 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 b₁ being Subset of (REAL n) st
for x being object holds
( x in b₁ 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 b₁, b₂ being Subset of (REAL n) st ( for x being object holds
( x in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines OpenHyperInterval SRINGS_5:def 15 :
for n being Nat
for a, b being Element of REAL n
for b₄ being Subset of (REAL n) holds
( b₄ = OpenHyperInterval (a,b) iff for x being object holds
( x in b₄ 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 b₁ being Subset of (REAL n) st
for x being object holds
( x in b₁ 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 b₁, b₂ being Subset of (REAL n) st ( for x being object holds
( x in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines LeftOpenHyperInterval SRINGS_5:def 16 :
for n being Nat
for a, b being Element of REAL n
for b₄ being Subset of (REAL n) holds
( b₄ = LeftOpenHyperInterval (a,b) iff for x being object holds
( x in b₄ 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 b₁ being Subset of (REAL n) st
for x being object holds
( x in b₁ 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 b₁, b₂ being Subset of (REAL n) st ( for x being object holds
( x in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines RightOpenHyperInterval SRINGS_5:def 17 :
for n being Nat
for a, b being Element of REAL n
for b₄ being Subset of (REAL n) holds
( b₄ = RightOpenHyperInterval (a,b) iff for x being object holds
( x in b₄ 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;

cluster ClosedHyperInterval (a,a) -> trivial ;

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 (Euclid n) 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 (TOP-REAL n) 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 (ProductLeftOpenIntervals n) = 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 (ProductRightOpenIntervals n) = 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 b₁ being Function of [:(REAL n),(REAL n):],REAL st
for x, y being Element of REAL n holds b₁ . (x,y) = sup (rng (abs (x - y)))

proof end;

uniqueness
for b₁, b₂ being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b₁ . (x,y) = sup (rng (abs (x - y))) ) & ( for x, y being Element of REAL n holds b₂ . (x,y) = sup (rng (abs (x - y))) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines Infty_dist SRINGS_5:def 20 :
for n being non zero Nat
for b₂ being Function of [:(REAL n),(REAL n):],REAL holds
( b₂ = Infty_dist n iff for x, y being Element of REAL n holds b₂ . (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 } & (Infty_dist n) . (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 (Infty_dist n) . (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
( (Infty_dist n) . (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 (Infty_dist n) . (x,y) = (Infty_dist n) . (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 (Infty_dist n) . (x,y) <= ((Infty_dist n) . (x,z)) + ((Infty_dist n) . (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

(Pitag_dist 2) . (|[0,0]|,|[1,1]|) = sqrt 2

proof end;

theorem Th64: :: SRINGS_5:97

(Infty_dist 2) . (|[0,0]|,|[1,1]|) = 1

proof end;

theorem Th65: :: SRINGS_5:98

for x, y being Element of REAL 1 holds (Infty_dist 1) . (x,y) = |.((x . 1) - (y . 1)).|

proof end;

theorem Th66: :: SRINGS_5:99

for x, y being Element of REAL 1 holds (Pitag_dist 1) . (x,y) = |.((x . 1) - (y . 1)).|

proof end;

theorem :: SRINGS_5:100

Pitag_dist 1 = Infty_dist 1

proof end;

theorem :: SRINGS_5:101

Pitag_dist 2 <> Infty_dist 2

proof end;

definition

let n be non zero Nat;

func EMINFTY n -> strict MetrSpace equals :: SRINGS_5:def 21
MetrStruct(# (REAL n),(Infty_dist n) #);

coherence
MetrStruct(# (REAL n),(Infty_dist 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),(Infty_dist 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 (EMINFTY n) & RLSStruct(# the carrier of it, the ZeroF of it, the addF of it, the Mult of it #) = RealVectSpace (Seg n) );

existence
ex b₁ being strict RLTopStruct st
( TopStruct(# the carrier of b₁, the topology of b₁ #) = TopSpaceMetr (EMINFTY n) & RLSStruct(# the carrier of b₁, the ZeroF of b₁, the addF of b₁, the Mult of b₁ #) = RealVectSpace (Seg n) )

proof end;

uniqueness
for b₁, b₂ being strict RLTopStruct st TopStruct(# the carrier of b₁, the topology of b₁ #) = TopSpaceMetr (EMINFTY n) & RLSStruct(# the carrier of b₁, the ZeroF of b₁, the addF of b₁, the Mult of b₁ #) = RealVectSpace (Seg n) & TopStruct(# the carrier of b₂, the topology of b₂ #) = TopSpaceMetr (EMINFTY n) & RLSStruct(# the carrier of b₂, the ZeroF of b₂, the addF of b₂, the Mult of b₂ #) = RealVectSpace (Seg n) holds
b₁ = b₂ ;

end;

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

theorem :: SRINGS_5:102

for n being non zero Nat holds RLSStruct(# the carrier of (TOP-REAL n), the ZeroF of (TOP-REAL n), the addF of (TOP-REAL n), the Mult of (TOP-REAL n) #) = RLSStruct(# the carrier of (TOP-REAL-INFTY n), the ZeroF of (TOP-REAL-INFTY n), the addF of (TOP-REAL-INFTY n), the Mult of (TOP-REAL-INFTY n) #)

proof end;

registration

let n be non zero Nat;

cluster TOP-REAL-INFTY n -> non empty strict ;

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 (EMINFTY n);

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 (EMINFTY n) holds @ p = p;

theorem Th68: :: SRINGS_5:105

for r being Real
for n being non zero Nat
for p being Element of (EMINFTY n) 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 (EMINFTY n)
for e being Point of (Euclid n) st e = p holds
Ball (p,r) = OpenHypercube (e,r)

proof end;

registration

let n be non zero Nat;
let p be Element of (EMINFTY n);
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 (EMINFTY n)
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 (TOP-REAL n)
for q being Element of (EMINFTY n) 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 (EMINFTY n) 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 (EMINFTY n) holds cl_Ball (p,r) = ClosedHyperInterval (((@ p) - (n |-> r)),((@ p) + (n |-> r)))

proof end;