:: by Roland Coghetto

::

:: Received December 31, 2015

:: Copyright (c) 2015-2018 Association of Mizar Users

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

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

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_{1} -element FinSequence

for X being non empty set

for f being Function st f = (Seg n) --> X holds

f is non-empty b

proof end;

definition
end;

:: deftheorem defines ProductREAL SRINGS_5:def 1 :

for n being Nat holds ProductREAL n = (Seg n) --> REAL;

for n being Nat holds ProductREAL n = (Seg n) --> REAL;

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 )

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 }

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)

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)

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

redefine func x `2 -> Element of REAL ;

coherence

x `2 is Element of REAL

end;
:: original: `1

redefine func x `1 -> Element of REAL ;

coherence

x `1 is Element of REAL

proof end;

:: original: `2redefine func x `2 -> Element of REAL ;

coherence

x `2 is Element of REAL

proof 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

redefine func x `2 -> Element of REAL n;

coherence

x `2 is Element of REAL n

end;
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: `2redefine func x `2 -> Element of REAL n;

coherence

x `2 is Element of REAL n

proof end;

theorem Th13: :: SRINGS_5:16

for n being Nat

for f being b_{1} -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 )

for f being b

for i being Nat st i in Seg n holds

( (x `1) . i = (f /. i) `1 & (x `2) . i = (f /. i) `2 )

proof end;

registration
end;

registration
end;

registration
end;

registration

let n be Nat;

coherence

for b_{1} being Subset of (TOP-REAL n) st b_{1} = RAT n holds

( b_{1} is countable & b_{1} is dense )
by Th15;

end;
coherence

for b

( b

registration
end;

registration
end;

definition

let n be Nat;

{ (OpenHypercubes q) where q is Point of (Euclid n) : q in RAT n } is non empty set

end;
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 } ;

{ (OpenHypercubes q) where q is Point of (Euclid n) : q in RAT n } is non empty set

proof 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 } ;

for n being Nat holds OpenHypercubesRAT n = { (OpenHypercubes q) where q is Point of (Euclid n) : q in RAT n } ;

definition
end;

:: deftheorem defines @ SRINGS_5:def 4 :

for n being Nat

for q being Element of RAT n holds @ q = q;

for n being Nat

for q being Element of RAT n holds @ q = q;

definition
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;

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;

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

proof end;

Th18: for n being Nat holds union (OpenHypercubesRAT n) is 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

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

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;

definition

let n be Nat;

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

end;
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);

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

:: deftheorem defines dense_countable_OpenHypercubes SRINGS_5:def 6 :

for n being Nat holds dense_countable_OpenHypercubes n = union (OpenHypercubesRAT n);

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
end;

theorem :: SRINGS_5:23

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 )

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

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

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

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

{ ].a,b.] where a, b is Real : verum } is Subset-Family of REAL
end;

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 } ;

{ ].a,b.] where a, b is Real : verum } is Subset-Family of REAL

proof 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 } ;

the_set_of_all_left_open_real_bounded_intervals = { ].a,b.] where a, b is Real : verum } ;

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

definition

{ [.a,b.[ where a, b is Real : verum } is Subset-Family of REAL
end;

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 } ;

{ [.a,b.[ where a, b is Real : verum } is Subset-Family of REAL

proof 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 } ;

the_set_of_all_right_open_real_bounded_intervals = { [.a,b.[ where a, b is Real : verum } ;

registration
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

( 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;

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;

theorem :: SRINGS_5:32

definition

let n be non zero Nat;

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

end;
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;

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

proof 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;

for n being non zero Nat holds ProductLeftOpenIntervals n = (Seg n) --> the_set_of_all_left_open_real_bounded_intervals;

theorem :: SRINGS_5:33

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.] ) )

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_{1} -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).] ) ) )

for x being object st x in MeasurableRectangle (ProductLeftOpenIntervals n) holds

ex y being Subset of (REAL n) ex f being b

( 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).] ) ) ) ) )

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).] )

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;

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

end;
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;

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

proof 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;

for n being non zero Nat holds ProductRightOpenIntervals n = (Seg n) --> the_set_of_all_right_open_real_bounded_intervals;

theorem :: SRINGS_5:39

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.[ ) )

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_{1} -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).[ ) ) )

for x being object st x in MeasurableRectangle (ProductRightOpenIntervals n) holds

ex y being Subset of (REAL n) ex f being b

( 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).[ ) ) ) ) )

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).[ )

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 ;

ex b_{1} being set st

for f being object holds

( f in b_{1} iff ex g being Function st

( f = product g & g in product ((Seg n) --> X) ) )

for b_{1}, b_{2} being set st ( for f being object holds

( f in b_{1} iff ex g being Function st

( f = product g & g in product ((Seg n) --> X) ) ) ) & ( for f being object holds

( f in b_{2} iff ex g being Function st

( f = product g & g in product ((Seg n) --> X) ) ) ) holds

b_{1} = b_{2}

end;
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 for f being object holds

( f in it iff ex g being Function st

( f = product g & g in product ((Seg n) --> X) ) );

ex b

for f being object holds

( f in b

( f = product g & g in product ((Seg n) --> X) ) )

proof end;

uniqueness for b

( f in b

( f = product g & g in product ((Seg n) --> X) ) ) ) & ( for f being object holds

( f in b

( f = product g & g in product ((Seg n) --> X) ) ) ) holds

b

proof end;

:: deftheorem Def2 defines Product SRINGS_5:def 11 :

for n being Nat

for X, b_{3} being set holds

( b_{3} = Product (n,X) iff for f being object holds

( f in b_{3} iff ex g being Function st

( f = product g & g in product ((Seg n) --> X) ) ) );

for n being Nat

for X, b

( b

( f in b

( 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)))))

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

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 }

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

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)

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

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

{ [.a,b.] where a, b is Real : verum } is Subset-Family of REAL
end;

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 } ;

{ [.a,b.] where a, b is Real : verum } is Subset-Family of REAL

proof 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 } ;

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

( 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 )
end;

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;

theorem :: SRINGS_5:53

for n being Nat holds (Seg n) --> the_set_of_all_closed_real_bounded_intervals is b_{1} -element FinSequence

proof end;

definition

{ ].a,b.[ where a, b is Real : verum } is Subset-Family of REAL
end;

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 } ;

{ ].a,b.[ where a, b is Real : verum } is Subset-Family of REAL

proof 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 } ;

the_set_of_all_open_real_bounded_intervals = { ].a,b.[ where a, b is Real : verum } ;

registration

( 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 )
end;

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;

theorem :: SRINGS_5:55

for n being Nat holds (Seg n) --> the_set_of_all_open_real_bounded_intervals is b_{1} -element FinSequence

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

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

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).]

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).] )

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)

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)

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)

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).]

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).] )

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).[

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).[ )

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;

ex b_{1} being Subset of (REAL n) st

for x being object holds

( x in b_{1} 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 b_{1}, b_{2} being Subset of (REAL n) st ( for x being object holds

( x in b_{1} 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_{2} 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_{1} = b_{2}

end;
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 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).] ) ) );

ex b

for x being object holds

( x in b

( x = y & ( for i being Nat st i in Seg n holds

y . i in [.(a . i),(b . i).] ) ) )

proof end;

uniqueness for b

( x in b

( 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

( x = y & ( for i being Nat st i in Seg n holds

y . i in [.(a . i),(b . i).] ) ) ) ) holds

b

proof end;

:: deftheorem Def3 defines ClosedHyperInterval SRINGS_5:def 14 :

for n being Nat

for a, b being Element of REAL n

for b_{4} being Subset of (REAL n) holds

( b_{4} = ClosedHyperInterval (a,b) iff for x being object holds

( x in b_{4} 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 n being Nat

for a, b being Element of REAL n

for b

( b

( x in b

( 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;

ex b_{1} being Subset of (REAL n) st

for x being object holds

( x in b_{1} 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 b_{1}, b_{2} being Subset of (REAL n) st ( for x being object holds

( x in b_{1} 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_{2} 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_{1} = b_{2}

end;
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 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).[ ) ) );

ex b

for x being object holds

( x in b

( x = y & ( for i being Nat st i in Seg n holds

y . i in ].(a . i),(b . i).[ ) ) )

proof end;

uniqueness for b

( x in b

( 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

( x = y & ( for i being Nat st i in Seg n holds

y . i in ].(a . i),(b . i).[ ) ) ) ) holds

b

proof end;

:: deftheorem Def4 defines OpenHyperInterval SRINGS_5:def 15 :

for n being Nat

for a, b being Element of REAL n

for b_{4} being Subset of (REAL n) holds

( b_{4} = OpenHyperInterval (a,b) iff for x being object holds

( x in b_{4} 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 n being Nat

for a, b being Element of REAL n

for b

( b

( x in b

( 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;

ex b_{1} being Subset of (REAL n) st

for x being object holds

( x in b_{1} 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 b_{1}, b_{2} being Subset of (REAL n) st ( for x being object holds

( x in b_{1} 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_{2} 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_{1} = b_{2}

end;
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 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).] ) ) );

ex b

for x being object holds

( x in b

( x = y & ( for i being Nat st i in Seg n holds

y . i in ].(a . i),(b . i).] ) ) )

proof end;

uniqueness for b

( x in b

( 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

( x = y & ( for i being Nat st i in Seg n holds

y . i in ].(a . i),(b . i).] ) ) ) ) holds

b

proof end;

:: deftheorem Def5 defines LeftOpenHyperInterval SRINGS_5:def 16 :

for n being Nat

for a, b being Element of REAL n

for b_{4} being Subset of (REAL n) holds

( b_{4} = LeftOpenHyperInterval (a,b) iff for x being object holds

( x in b_{4} 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 n being Nat

for a, b being Element of REAL n

for b

( b

( x in b

( 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;

ex b_{1} being Subset of (REAL n) st

for x being object holds

( x in b_{1} 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 b_{1}, b_{2} being Subset of (REAL n) st ( for x being object holds

( x in b_{1} 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_{2} 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_{1} = b_{2}

end;
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 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).[ ) ) );

ex b

for x being object holds

( x in b

( x = y & ( for i being Nat st i in Seg n holds

y . i in [.(a . i),(b . i).[ ) ) )

proof end;

uniqueness for b

( x in b

( 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

( x = y & ( for i being Nat st i in Seg n holds

y . i in [.(a . i),(b . i).[ ) ) ) ) holds

b

proof end;

:: deftheorem Def6 defines RightOpenHyperInterval SRINGS_5:def 17 :

for n being Nat

for a, b being Element of REAL n

for b_{4} being Subset of (REAL n) holds

( b_{4} = RightOpenHyperInterval (a,b) iff for x being object holds

( x in b_{4} 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 n being Nat

for a, b being Element of REAL n

for b

( b

( x in b

( x = y & ( for i being Nat st i in Seg n holds

y . i in [.(a . i),(b . i).[ ) ) ) );

registration
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) )

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;

reflexivity

for a being Element of REAL n

for i being Nat st i in Seg n holds

a . i <= a . i ;

end;
let a, b be Element of REAL n;

reflexivity

for a being Element of REAL n

for i being Nat st i in Seg n holds

a . i <= a . i ;

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

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

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

for a, b being Element of REAL n st a <= b holds

not ClosedHyperInterval (a,b) is empty

proof 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 );

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

for a, b being Element of REAL n st b < a & not n is zero holds

ClosedHyperInterval (a,b) is empty

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;
let r be Real;

:: original: |->

redefine func n |-> r -> Element of REAL n;

coherence

n |-> r is Element of REAL n by Th50;

definition

let r be Real;

:: original: <*

redefine func <*r*> -> Element of REAL 1;

coherence

<*r*> is Element of REAL 1

end;
:: original: <*

redefine func <*r*> -> Element of REAL 1;

coherence

<*r*> is Element of REAL 1

proof 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))) )

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

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 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).[

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).[ )

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).]

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).] )

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).[

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).[ )

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;

ex b_{1} being Function of [:(REAL n),(REAL n):],REAL st

for x, y being Element of REAL n holds b_{1} . (x,y) = sup (rng (abs (x - y)))

for b_{1}, b_{2} being Function of [:(REAL n),(REAL n):],REAL st ( for x, y being Element of REAL n holds b_{1} . (x,y) = sup (rng (abs (x - y))) ) & ( for x, y being Element of REAL n holds b_{2} . (x,y) = sup (rng (abs (x - y))) ) holds

b_{1} = b_{2}

end;
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 for x, y being Element of REAL n holds it . (x,y) = sup (rng (abs (x - y)));

ex b

for x, y being Element of REAL n holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def7 defines Infty_dist SRINGS_5:def 20 :

for n being non zero Nat

for b_{2} being Function of [:(REAL n),(REAL n):],REAL holds

( b_{2} = Infty_dist n iff for x, y being Element of REAL n holds b_{2} . (x,y) = sup (rng (abs (x - y))) );

for n being non zero Nat

for b

( b

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

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 )

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

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 )

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)

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

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;

definition

let n be non zero Nat;

MetrStruct(# (REAL n),(Infty_dist n) #) is strict MetrSpace

end;
func EMINFTY n -> strict MetrSpace equals :: SRINGS_5:def 21

MetrStruct(# (REAL n),(Infty_dist n) #);

coherence MetrStruct(# (REAL n),(Infty_dist n) #);

MetrStruct(# (REAL n),(Infty_dist n) #) is strict MetrSpace

proof end;

:: deftheorem defines EMINFTY SRINGS_5:def 21 :

for n being non zero Nat holds EMINFTY n = MetrStruct(# (REAL n),(Infty_dist n) #);

for n being non zero Nat holds EMINFTY n = MetrStruct(# (REAL n),(Infty_dist n) #);

registration
end;

definition

let n be non zero Nat;

ex b_{1} being strict RLTopStruct st

( TopStruct(# the carrier of b_{1}, the topology of b_{1} #) = TopSpaceMetr (EMINFTY n) & RLSStruct(# the carrier of b_{1}, the ZeroF of b_{1}, the addF of b_{1}, the Mult of b_{1} #) = RealVectSpace (Seg n) )

for b_{1}, b_{2} being strict RLTopStruct st TopStruct(# the carrier of b_{1}, the topology of b_{1} #) = TopSpaceMetr (EMINFTY n) & RLSStruct(# the carrier of b_{1}, the ZeroF of b_{1}, the addF of b_{1}, the Mult of b_{1} #) = RealVectSpace (Seg n) & TopStruct(# the carrier of b_{2}, the topology of b_{2} #) = TopSpaceMetr (EMINFTY n) & RLSStruct(# the carrier of b_{2}, the ZeroF of b_{2}, the addF of b_{2}, the Mult of b_{2} #) = RealVectSpace (Seg n) holds

b_{1} = b_{2}
;

end;
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 ( 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) );

ex b

( TopStruct(# the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def8 defines TOP-REAL-INFTY SRINGS_5:def 22 :

for n being non zero Nat

for b_{2} being strict RLTopStruct holds

( b_{2} = TOP-REAL-INFTY n iff ( TopStruct(# the carrier of b_{2}, the topology of b_{2} #) = TopSpaceMetr (EMINFTY n) & RLSStruct(# the carrier of b_{2}, the ZeroF of b_{2}, the addF of b_{2}, the Mult of b_{2} #) = RealVectSpace (Seg n) ) );

for n being non zero Nat

for b

( b

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;

theorem :: SRINGS_5:103

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

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
end;

:: deftheorem defines @ SRINGS_5:def 23 :

for n being non zero Nat

for p being Element of (EMINFTY n) holds @ p = p;

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

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)

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;

coherence

cl_Ball (p,r) is empty

end;
let p be Element of (EMINFTY n);

let r be negative Real;

coherence

cl_Ball (p,r) is empty

proof 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).] ) ) )

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

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

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

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;