:: Chebyshev Distance
:: by Roland Coghetto
::
:: Received December 31, 2015
:: Copyright (c) 2015-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RLVECT_1, RVSUM_1, ALGSTR_0, METRIC_1, SQUARE_1, VALUED_0,
PRE_TOPC, EQREL_1, PROB_1, MEASURE5, SUPINF_1, XREAL_0, MCART_1,
XBOOLE_0, ORDINAL1, FINSEQ_2, EUCLID_9, ARYTM_3, XCMPLX_0, EUCLID,
RCOMP_1, PCOMPS_1, SUBSET_1, TARSKI, NAT_1, NUMBERS, CARD_1, CARD_3,
TOPS_1, REAL_1, TOPMETR, RELAT_1, FUNCT_1, FINSEQ_1, XXREAL_0, ARYTM_1,
XXREAL_1, QC_LANG1, FUNCT_2, FINSET_1, CANTOR_1, RLVECT_3, SETFAM_1,
ZFMISC_1, STRUCT_0, FUNCOP_1, SRINGS_3, SRINGS_4, SRINGS_1, FINSUB_1,
SIMPLEX0, PARTFUN1, COMPLEX1, TIETZE_2, ORDINAL2, XXREAL_2, FUNCT_7,
MEMBERED, RLTOPSP1, FUNCSDOM, SRINGS_5;
notations SQUARE_1, ALGSTR_0, RLVECT_1, XXREAL_3, EXTREAL1, VALUED_1, RVSUM_1,
EQREL_1, MEASURE5, SUPINF_1, ZFMISC_1, FINSUB_1, SIMPLEX0, SUBSET_1,
NUMBERS, XXREAL_0, SETFAM_1, XREAL_0, RCOMP_1, TARSKI, ORDINAL1,
XCMPLX_0, PCOMPS_1, EUCLID_9, PRE_TOPC, FINSEQ_2, CARD_1, XBOOLE_0,
CARD_3, TOPS_1, TOPMETR, FUNCT_1, FINSEQ_1, TOPS_2, CANTOR_1, RELAT_1,
FINSET_1, FUNCT_2, FUNCOP_1, RELSET_1, NAT_1, STRUCT_0, TIETZE_2,
SRINGS_1, SRINGS_3, SRINGS_4, PARTFUN1, XTUPLE_0, PROB_1, COMPLEX1,
VALUED_0, XXREAL_2, MEMBERED, BINOP_1, METRIC_1, EUCLID, RLTOPSP1,
FUNCSDOM;
constructors SQUARE_1, SUPINF_2, EXTREAL1, EUCLID_9, TOPS_1, FUNCSDOM,
MONOID_0, TOPGEN_2, TIETZE_2, SRINGS_1, SRINGS_3, SRINGS_4, TOPGEN_3,
COMPLEX1, INTEGRA1, WAYBEL23;
registrations METRIC_1, XXREAL_1, FINSEQ_1, SUBSET_1, XREAL_0, NAT_1,
ORDINAL1, NUMBERS, FINSEQ_2, TOPGEN_4, CARD_1, EUCLID_9, TOPS_1,
XXREAL_0, EUCLID, VALUED_0, MONOID_0, RCOMP_1, CARD_3, FINSET_1,
RELSET_1, SRINGS_1, SRINGS_3, SRINGS_4, XCMPLX_0, XTUPLE_0, FUNCT_1,
FUNCT_2, SETFAM_1, MEMBERED, STRUCT_0, XXREAL_2, SQUARE_1, RLTOPSP1,
XBOOLE_0, MFOLD_0;
requirements SUBSET, NUMERALS, BOOLE, ARITHM, REAL;
begin :: Preliminaries
reserve n for Nat,
r,s for Real,
x,y for Element of REAL n,
p,q for Point of TOP-REAL n,
e for Point of Euclid n;
theorem :: SRINGS_5:1
abs (x-y) = abs (y-x);
theorem :: SRINGS_5:2
for i being Nat st i in Seg n holds abs x.i in REAL;
theorem :: SRINGS_5:3
for x,y being Element of REAL,xe,ye being ExtReal st x <= xe & y <= ye holds
x + y <= xe + ye;
theorem :: SRINGS_5:4
for a,c being Real, b being R_eal st a < b & [.a,b.[ c= [.a,c.[ holds
b is Real;
theorem :: SRINGS_5:5
for D being non empty set, D1 being non empty Subset of D holds
n-tuples_on D1 c= n-tuples_on D;
theorem :: SRINGS_5:6
for X being non empty set,f being Function st f = Seg n --> X holds
f is non-empty n-element FinSequence;
definition
let n be Nat;
func ProductREAL(n) -> non-empty n-element FinSequence equals
:: SRINGS_5:def 1
Seg n --> REAL;
end;
theorem :: SRINGS_5:7
ProductREAL(n) = Seg n --> the carrier of R^1;
theorem :: SRINGS_5:8
product (Seg n --> REAL) = REAL n;
theorem :: SRINGS_5:9
product ProductREAL(n) = REAL n;
theorem :: SRINGS_5:10
for X being set holds product(Seg n --> X) = n-tuples_on X;
theorem :: SRINGS_5:11
for D being non empty set, x being Tuple of n, D holds x in Funcs(Seg n,D);
theorem :: SRINGS_5:12
for O1 being Subset of TOP-REAL n, O2 being Subset of TopSpaceMetr Euclid n
st O1 = O2 holds O1 is open iff O2 is open;
theorem :: SRINGS_5:13
e = p implies
the set of all OpenHypercube(e,1/m) where m is non zero Element of NAT =
the set of all OpenHypercube(p,1/m) where m is non zero Element of NAT;
theorem :: SRINGS_5:14
q in OpenHypercube(p,r) implies p in OpenHypercube(q,r);
theorem :: SRINGS_5:15
q in OpenHypercube(p,r/2) implies OpenHypercube(q,r/2) c= OpenHypercube(p,r);
definition
let x be Element of [:REAL,REAL:];
redefine func x`1 -> Element of REAL;
redefine func x`2 -> Element of REAL;
end;
definition
let n be Nat, x be Element of [:REAL n,REAL n:];
redefine func x`1 -> Element of REAL n;
redefine func x`2 -> Element of REAL n;
end;
theorem :: SRINGS_5:16
for f being n-element FinSequence of [:REAL,REAL:] holds
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;
begin :: The set of n-tuples of rational numbers
definition
let n;
func RAT n -> FinSequenceSet of RAT equals
:: SRINGS_5:def 2
n-tuples_on RAT;
end;
theorem :: SRINGS_5:17
RAT 0 = {0};
registration
cluster RAT 0 -> trivial;
end;
registration
let n;
cluster RAT n -> non empty;
end;
registration
let n;
cluster -> n-element for Element of RAT n;
end;
registration
let n;
cluster RAT n -> countable;
end;
registration
let n be positive Nat;
cluster RAT n -> infinite;
end;
registration
let n be positive Nat;
cluster RAT n -> denumerable;
end;
theorem :: SRINGS_5:18
RAT n is dense Subset of TOP-REAL n;
registration
let n;
cluster RAT n -> countable dense for Subset of TOP-REAL n;
end;
begin :: A countable base of an n-dimensional Euclidean space (Version 1: MFOLD_1)
registration
let n be Nat;
cluster countable for Basis of TOP-REAL n;
end;
begin :: A countable base of an n-dimensional Euclidean space (Version 2)
registration
let n,e;
cluster OpenHypercubes(e) -> countable;
end;
definition
let n;
func OpenHypercubesRAT(n) -> non empty set equals
:: SRINGS_5:def 3
{OpenHypercubes(q) where q is Point of Euclid n : q in RAT n};
end;
definition
let n;
let q be Element of RAT n;
func @q -> Point of Euclid n equals
:: SRINGS_5:def 4
q;
end;
definition
let n;
let q be object such that
q in RAT n;
func object2RAT(q,n) -> Element of RAT n equals
:: SRINGS_5:def 5
q;
end;
registration let n;
cluster OpenHypercubesRAT(n) -> countable;
end;
registration let n;
cluster union OpenHypercubesRAT(n) -> countable;
end;
theorem :: SRINGS_5:19
union OpenHypercubesRAT(n) is open Subset-Family of TOP-REAL n;
theorem :: SRINGS_5:20
for O being non empty open Subset of TOP-REAL n holds
ex p being Element of RAT n st p in O;
theorem :: SRINGS_5:21
for cB being Subset-Family of TOP-REAL n st
cB = union OpenHypercubesRAT(n) holds cB is quasi_basis;
registration let n;
cluster union OpenHypercubesRAT(n) -> non empty;
end;
definition
let n;
func dense_countable_OpenHypercubes(n) -> countable open
Subset-Family of TOP-REAL n equals
:: SRINGS_5:def 6
union OpenHypercubesRAT(n);
end;
theorem :: SRINGS_5:22
dense_countable_OpenHypercubes(n) =
{OpenHypercube(q,1/m) where q is Point of Euclid n,
m is positive Nat:q in RAT n};
registration :: Second version
let n be Nat;
cluster countable for Basis of TOP-REAL n;
end;
theorem :: SRINGS_5:23
dense_countable_OpenHypercubes(n) is countable Basis of TOP-REAL n;
theorem :: SRINGS_5:24
for O being open Subset of TOP-REAL n holds
ex Y being Subset of dense_countable_OpenHypercubes(n) st Y is countable &
O = union Y;
theorem :: SRINGS_5:25
for O being open non empty Subset of TOP-REAL n holds
ex Y being Subset of dense_countable_OpenHypercubes(n) st Y is non 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;
theorem :: SRINGS_5:26
for O being open non empty Subset of TOP-REAL n holds
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;
theorem :: SRINGS_5:27
for O being open non empty Subset of TOP-REAL n holds
ex s being sequence of dense_countable_OpenHypercubes(n) st O = Union s;
begin :: The set of all left open real bounded interval
definition
func the_set_of_all_left_open_real_bounded_intervals
-> Subset-Family of REAL equals
:: SRINGS_5:def 7
the set of all ].a,b.] where a,b is Real;
end;
registration
cluster the_set_of_all_left_open_real_bounded_intervals ->
non empty;
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};
theorem :: SRINGS_5:29
the_set_of_all_left_open_real_bounded_intervals is
cap-closed
diff-finite-partition-closed with_empty_element
with_countable_Cover;
theorem :: SRINGS_5:30
the_set_of_all_left_open_real_bounded_intervals is Semiring of REAL;
begin :: The set of all right open real bounded interval
definition
func the_set_of_all_right_open_real_bounded_intervals
-> Subset-Family of REAL equals
:: SRINGS_5:def 8
the set of all [.a,b.[ where a,b is Real;
end;
registration
cluster the_set_of_all_right_open_real_bounded_intervals ->
non empty;
end;
theorem :: 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};
theorem :: SRINGS_5:32 :::
the_set_of_all_right_open_real_bounded_intervals is with_empty_element;
theorem :: SRINGS_5:33
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 with_empty_element;
theorem :: SRINGS_5:34 :::
the_set_of_all_right_open_real_bounded_intervals is with_countable_Cover;
theorem :: SRINGS_5:35
the_set_of_all_right_open_real_bounded_intervals is Semiring of REAL;
begin :: Finite Product of Left_Open_Intervals
reserve n for non zero Nat;
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;
end;
theorem :: SRINGS_5:36
ProductLeftOpenIntervals(n) = Seg n --> the set of all ].a,b.] where
a,b is Real;
theorem :: SRINGS_5:37
MeasurableRectangle(ProductLeftOpenIntervals(n)) is Semiring of REAL n;
theorem :: SRINGS_5:38
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.];
theorem :: SRINGS_5:39
for x being object st x in MeasurableRectangle(ProductLeftOpenIntervals(n))
holds ex y being Subset of REAL n,
f being n-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.]);
theorem :: SRINGS_5:40
for x being object st x in MeasurableRectangle(ProductLeftOpenIntervals(n))
holds ex y being Subset of REAL n, 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 .]);
theorem :: SRINGS_5:41
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 .]);
begin :: Finite Product of Right_Open_Intervals
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;
end;
reserve n for non zero Nat;
theorem :: SRINGS_5:42
ProductRightOpenIntervals(n) = Seg n --> the set of all [.a,b.[ where
a,b is Real;
theorem :: SRINGS_5:43
MeasurableRectangle(ProductRightOpenIntervals(n)) is Semiring of REAL n;
theorem :: SRINGS_5:44
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.[;
theorem :: SRINGS_5:45
for x being object st x in MeasurableRectangle(ProductRightOpenIntervals(n))
holds ex y being Subset of REAL n,
f being n-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.[);
theorem :: SRINGS_5:46
for x being object st x in MeasurableRectangle(ProductRightOpenIntervals(n))
holds ex y being Subset of REAL n, 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 .[);
theorem :: SRINGS_5:47
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 .[);
begin :: n-dimensional product of Subset-Family
reserve n for Nat,
X for set,
S for Subset-Family of X;
definition
let n,X;
func Product(n,X) -> set means
:: 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);
end;
theorem :: SRINGS_5:48
Product(n,X) c= bool Funcs(dom (Seg n --> X), union Union (Seg n --> X));
theorem :: SRINGS_5:49
Product(n,S) is Subset-Family of product (Seg n --> X);
theorem :: SRINGS_5:50
for S being non empty Subset-Family of X holds
Product(n,S) = the set of all product f where f is Tuple of n,S;
theorem :: SRINGS_5:51
for n being non zero Nat holds
Product(n,X) c= bool Funcs(Seg n, union X);
theorem :: SRINGS_5:52
for n being non zero Nat, X being non empty set,
S being non empty Subset-Family of X st S <> {{}} holds
Product(n,S) c= bool Funcs(Seg n,X);
theorem :: SRINGS_5:53
for n being non zero Nat,X being non empty set,
S being non empty Subset-Family of X st S <> {{}} holds
union Product(n,S) c= Funcs(Seg n,X);
registration
let n be Nat, X be non empty set;
cluster Product(n,X) -> non empty;
end;
theorem :: SRINGS_5:54
for X being non empty set,
S being non empty Subset-Family of X,
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);
begin :: the set of all closed real bounded intervals
definition
func the_set_of_all_closed_real_bounded_intervals ->
Subset-Family of REAL equals
:: SRINGS_5:def 12
the set of all [.a,b.] where a,b is Real;
end;
theorem :: SRINGS_5:55
the_set_of_all_closed_real_bounded_intervals =
{I where I is Subset of REAL : I is closed_interval};
registration
cluster the_set_of_all_closed_real_bounded_intervals -> non empty;
end;
theorem :: SRINGS_5:56
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;
theorem :: SRINGS_5:57
for n being Nat holds Seg n -->
the_set_of_all_closed_real_bounded_intervals is n-element FinSequence;
begin :: The set of all open real bounded intervals
definition
func the_set_of_all_open_real_bounded_intervals ->
Subset-Family of REAL equals
:: SRINGS_5:def 13
the set of all ].a,b.[ where a,b is Real;
end;
theorem :: SRINGS_5:58
the_set_of_all_open_real_bounded_intervals c=
{I where I is Subset of REAL : I is open_interval};
registration
cluster the_set_of_all_open_real_bounded_intervals -> non empty;
end;
theorem :: SRINGS_5:59
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;
theorem :: SRINGS_5:60
for n being Nat holds Seg n --> the_set_of_all_open_real_bounded_intervals is
n-element FinSequence;
begin :: n-dimensional Subset-Family of REAL
reserve n for Nat,
S for Subset-Family of REAL;
theorem :: SRINGS_5:61
Product(n,S) is Subset-Family of REAL n;
definition
let n,S;
redefine func Product(n,S) -> Subset-Family of REAL n;
end;
theorem :: SRINGS_5:62
for S being non empty Subset-Family of REAL, 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;
theorem :: SRINGS_5:63
for n being non zero Nat,
s being Tuple of n,the_set_of_all_closed_real_bounded_intervals holds
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.];
theorem :: SRINGS_5:64
for n being non zero Nat,
x being Element of Product(n,the_set_of_all_closed_real_bounded_intervals)
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 .])));
theorem :: SRINGS_5:65
for n being non zero Nat, x being Subset of REAL n,
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);
theorem :: SRINGS_5:66
for n being non zero Nat, x being Subset of REAL n,
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);
theorem :: SRINGS_5:67
for n being non zero Nat,
x being Subset of REAL n,
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);
theorem :: SRINGS_5:68
for n being non zero Nat,
s being Tuple of n,the_set_of_all_left_open_real_bounded_intervals holds
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.];
theorem :: SRINGS_5:69
for n being non zero Nat,
x being Element of
Product(n,the_set_of_all_left_open_real_bounded_intervals)
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 .])));
theorem :: SRINGS_5:70
for n being non zero Nat,
s being Tuple of n,the_set_of_all_right_open_real_bounded_intervals holds
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.[;
theorem :: SRINGS_5:71
for n being non zero Nat,
x being Element of
Product(n,the_set_of_all_right_open_real_bounded_intervals)
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 .[)));
begin :: Closed/Open/LeftOpen/RightOpen - HyperInterval
reserve n for Nat,
a,b,c,d for Element of REAL n;
definition
let n,a,b;
func ClosedHyperInterval(a,b) -> Subset of REAL n means
:: 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.]);
end;
definition
let n,a,b;
func OpenHyperInterval(a,b) -> Subset of REAL n means
:: 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.[);
end;
definition
let n,a,b;
func LeftOpenHyperInterval(a,b) -> Subset of REAL n means
:: 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.]);
end;
definition
let n,a,b;
func RightOpenHyperInterval(a,b) -> Subset of REAL n means
:: 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.[);
end;
theorem :: SRINGS_5:72
ClosedHyperInterval(a,a) = {a};
registration
let n,a;
cluster ClosedHyperInterval(a,a) -> trivial;
end;
theorem :: SRINGS_5:73
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);
definition
let n,a,b;
pred a <= b means
:: SRINGS_5:def 18
for i being Nat st i in Seg n holds a.i <= b.i;
reflexivity;
end;
theorem :: SRINGS_5:74
a <= b & b <= c implies a <= c;
theorem :: SRINGS_5:75
a <= c & d <= b implies ClosedHyperInterval(c,d) c= ClosedHyperInterval(a,b);
theorem :: SRINGS_5:76
a <= b implies ClosedHyperInterval(a,b) is non empty;
definition
let n,a,b;
pred a < b means
:: SRINGS_5:def 19
for i being Nat st i in Seg n holds a.i < b.i;
end;
theorem :: SRINGS_5:77
a < b & b < c implies a < c;
theorem :: SRINGS_5:78
b < a & n is non zero implies ClosedHyperInterval(a,b) is empty;
theorem :: SRINGS_5:79
n|-> r is Element of REAL n;
definition
let n,r;
redefine func n |-> r -> Element of REAL n;
end;
definition
let r;
redefine func <*r*> -> Element of REAL 1;
end;
theorem :: SRINGS_5:80
for n being non zero Nat,e being Point of Euclid n
holds ex a being Element of REAL n st a = e &
OpenHypercube(e,r) = OpenHyperInterval(a - (n|-> r),a + (n|-> r));
theorem :: SRINGS_5:81
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);
begin :: Correspondance between Interval and 1-dimensional HyperInterval
theorem :: SRINGS_5:82
for x being Real holds x in [.r,s.] iff
1 |-> x in ClosedHyperInterval(<*r*>,<*s*>);
theorem :: SRINGS_5:83
for x being Real holds x in ].r,s.[ iff
1 |-> x in OpenHyperInterval(<*r*>,<*s*>);
theorem :: SRINGS_5:84
for x being Real holds x in ].r,s.] iff
1 |-> x in LeftOpenHyperInterval(<*r*>,<*s*>);
theorem :: SRINGS_5:85
for x being Real holds x in [.r,s.[ iff
1 |-> x in RightOpenHyperInterval(<*r*>,<*s*>);
begin :: Correspondance between MeasurableRectangle and Product
reserve n for non zero Nat;
theorem :: SRINGS_5:86
for s being Tuple of n,the_set_of_all_open_real_bounded_intervals holds
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.[;
theorem :: SRINGS_5:87
for x being Element of Product(n,the_set_of_all_open_real_bounded_intervals)
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 .[)));
theorem :: SRINGS_5:88
for s being Tuple of n,the_set_of_all_left_open_real_bounded_intervals holds
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.];
theorem :: SRINGS_5:89
for x being Element of
Product(n,the_set_of_all_left_open_real_bounded_intervals)
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 .])));
theorem :: SRINGS_5:90
for s being Tuple of n,the_set_of_all_right_open_real_bounded_intervals holds
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.[;
theorem :: SRINGS_5:91
for x being Element of
Product(n,the_set_of_all_right_open_real_bounded_intervals)
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 .[)));
theorem :: SRINGS_5:92
MeasurableRectangle(ProductLeftOpenIntervals(n)) =
Product(n,the_set_of_all_left_open_real_bounded_intervals);
theorem :: SRINGS_5:93
MeasurableRectangle(ProductRightOpenIntervals(n)) =
Product(n,the_set_of_all_right_open_real_bounded_intervals);
begin :: Chebyshev distance
reserve n for non zero Nat,
x,y,z for Element of REAL n;
definition
let n;
func Infty_dist n -> Function of [:REAL n,REAL n:],REAL means
:: SRINGS_5:def 20
for x,y being Element of REAL n holds it.(x,y) = sup rng abs(x-y);
end;
theorem :: SRINGS_5:94
(the set of all |. x.i - y.i .| where
i is Element of Seg n) is real-membered &
(the set of all |. x.i - y.i .| where i is Element of Seg n) = rng abs(x-y);
theorem :: SRINGS_5:95
ex S being ext-real-membered set st S = the set of all |. x.i - y.i .| where
i is Element of Seg n & (Infty_dist n).(x,y) = sup S;
theorem :: SRINGS_5:96
(Infty_dist n).(x,y) = abs (x-y).max_diff_index(x,y);
theorem :: SRINGS_5:97
(Infty_dist n).(x,y) = 0 iff x = y;
theorem :: SRINGS_5:98
(Infty_dist n).(x,y) = (Infty_dist n).(y,x);
theorem :: SRINGS_5:99
(Infty_dist n).(x,y) <= (Infty_dist n).(x,z) + (Infty_dist n).(z,y);
theorem :: SRINGS_5:100
Infty_dist n is_metric_of REAL n;
theorem :: SRINGS_5:101
(Pitag_dist 2).(|[0,0]|,|[1,1]|) = sqrt 2;
theorem :: SRINGS_5:102
(Infty_dist 2).(|[0,0]|,|[1,1]|) = 1;
theorem :: SRINGS_5:103
for x,y being Element of REAL 1 holds (Infty_dist 1).(x,y) = |.x.1-y.1.|;
theorem :: SRINGS_5:104
for x,y being Element of REAL 1 holds (Pitag_dist 1).(x,y) = |.x.1-y.1.|;
theorem :: SRINGS_5:105
Pitag_dist 1 = Infty_dist 1;
theorem :: SRINGS_5:106
Pitag_dist 2 <> Infty_dist 2;
definition
let n being non zero Nat;
func EMINFTY n -> strict MetrSpace equals
:: SRINGS_5:def 21
MetrStruct(#REAL n,Infty_dist n#);
end;
registration
let n being non zero Nat;
cluster EMINFTY n -> non empty;
end;
definition
let n being non zero Nat;
func TOP-REAL-INFTY n -> strict RLTopStruct means
:: SRINGS_5:def 22
the TopStruct of it = TopSpaceMetr EMINFTY n &
the RLSStruct of it = RealVectSpace Seg n;
end;
theorem :: SRINGS_5:107
the RLSStruct of TOP-REAL n = the RLSStruct of TOP-REAL-INFTY n;
registration
let n being non zero Nat;
cluster TOP-REAL-INFTY n -> non empty;
end;
theorem :: SRINGS_5:108
for x being Element of REAL 0 holds Intervals(x,r) is empty &
product Intervals(x,r) = {{}};
theorem :: SRINGS_5:109
r <= 0 implies product Intervals(x,r) is empty;
reserve p for Element of EMINFTY n;
definition
let n being non zero Nat,
p being Element of EMINFTY n;
func @p -> Element of REAL n equals
:: SRINGS_5:def 23
p;
end;
theorem :: SRINGS_5:110
Ball(p,r) = product Intervals(@p,r);
theorem :: SRINGS_5:111
for e being Point of Euclid n st e = p holds Ball(p,r) = OpenHypercube(e,r);
registration
let n being non zero Nat,
p being Element of EMINFTY n,
r being negative Real;
cluster cl_Ball(p,r) -> empty;
end;
theorem :: SRINGS_5:112
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.];
theorem :: SRINGS_5:113
for p being Point of TOP-REAL n, q being Element of EMINFTY n st
q = p holds cl_Ball(q,r) = ClosedHypercube(p,n |-> r);
theorem :: SRINGS_5:114
Ball(p,r) = OpenHyperInterval(@p - (n|-> r), @p + (n|-> r));
theorem :: SRINGS_5:115
cl_Ball(p,r) = ClosedHyperInterval(@p - (n|-> r), @p + (n|-> r));