:: Chebyshev Distance
:: by Roland Coghetto
::
:: Received December 31, 2015
:: Copyright (c) 2015-2026 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;
definitions TARSKI, XBOOLE_0, TOPS_2;
equalities XCMPLX_0, METRIC_1, PCOMPS_1, TOPMETR, EUCLID, CARD_3, EUCLID_9,
FINSEQ_1, FUNCSDOM;
expansions XBOOLE_0, STRUCT_0, TARSKI, TOPS_2, PRE_TOPC;
theorems TBSP_1, JORDAN2B, EXTREAL1, XXREAL_3, VALUED_0, MEASURE5, FINSUB_1,
SETFAM_1, SRINGS_1, EUCLID_9, EUCLID, CARD_4, TOPS_1, NUMBERS, XBOOLE_0,
XBOOLE_1, MARGREL1, FINSEQ_1, FINSEQ_2, FUNCT_1, TOPGEN_1, XXREAL_0,
XREAL_1, XXREAL_1, ORDINAL1, CARD_3, CARD_1, BORSUK_5, CANTOR_1,
TIETZE_2, TOPGEN_4, NAT_1, XCMPLX_1, ZFMISC_1, TARSKI, FUNCT_2, WAYBEL12,
CARD_2, FUNCOP_1, PRE_TOPC, SCMYCIEL, SRINGS_3, SRINGS_4, CARD_5,
SRINGS_2, XREAL_0, PARTFUN1, REAL_NS1, ABSVALUE, RELSET_1, MESFUNC1,
FUNCT_5, FUNCT_6, RVSUM_1, XXREAL_2, SUBSET_1, BINOP_1, PCOMPS_1,
MEMBERED, VALUED_1, COMPLEX1, SQUARE_1, EUCLID_3, METRIC_1;
schemes FINSEQ_4, FUNCT_1, CARD_4, FINSEQ_1, XBOOLE_0, BINOP_1;
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 Th1:
abs (x-y) = abs (y-x)
proof
now
dom abs(x-y) = Seg n & dom abs(y-x) = Seg n by FINSEQ_2:124;
hence dom abs(x-y) = dom abs(y-x);
thus for i be object st i in dom abs(x-y) holds
abs(x-y).i = abs(y-x).i
proof
let i be object;
assume i in dom abs(x-y);
reconsider fxy = x-y,fyx = y - x as complex-valued Function;
A1: abs fxy.i = |.(x-y).i.| & abs fyx.i = |.(y-x).i.| by VALUED_1:18;
reconsider j = i as set by TARSKI:1;
reconsider rx = x,ry = y as Element of n-tuples_on REAL;
A2: (rx-ry).j = rx.j - ry.j & -(ry-rx).j = -(ry.j-rx.j) by RVSUM_1:27;
reconsider c1 = (x-y).i, c2 = (y-x).i as ExtReal;
A3: |.c2.| = |.-c2.| & c1 = -c2 by A2,XXREAL_3:def 3,EXTREAL1:29;
|.c1.| = |. (x-y).i qua Complex.| & |.c2.| = |.(y-x).i qua Complex.|
by EXTREAL1:12;
hence abs(x-y).i = abs(y-x).i by A1,A3;
end;
end;
hence thesis by FUNCT_1:def 11;
end;
theorem Th2:
for i being Nat st i in Seg n holds abs x.i in REAL
proof
let i be Nat;
assume
A1: i in Seg n;
reconsider f = x as complex-valued Function;
dom |.f.| = dom f & dom f = Seg n by FINSEQ_2:124,VALUED_1:def 11;
then rng |.f.| c= REAL & i in dom |.f.| by A1;
hence thesis by FUNCT_1:3;
end;
theorem Th3:
for x,y being Element of REAL,xe,ye being ExtReal st x <= xe & y <= ye holds
x + y <= xe + ye
proof
let x,y be Element of REAL,xe,ye be ExtReal;
assume that
A1: x <= xe and
A2: y <= ye;
reconsider x1 = x,y1 = y as ExtReal;
x1 + y1 <= xe + ye by A1,A2,XXREAL_3:36;
hence x + y <= xe + ye by XXREAL_3:def 2;
end;
theorem Th4:
for a,c being Real, b being R_eal st a < b & [.a,b.[ c= [.a,c.[ holds
b is Real
proof
let a,c be Real, b be R_eal;
assume that
A1: a < b and
A2: [.a,b.[ c= [.a,c.[;
set K = [.a,b.[;
A3: not c in K by A2,XXREAL_1:3;
per cases;
suppose
A4: K is non empty;
then consider x be object such that
A5: x in K;
reconsider x as Real by A5;
assume not b is Real;
then not b in REAL & a in REAL & a <= b by XREAL_0:def 1,A4,XXREAL_1:27;
then
A6: b = +infty by XXREAL_0:10;
a <= x by A5,XXREAL_1:3; then
A7: [.x,+infty.[ c= [.a,b.[ by A6,XXREAL_1:38;
per cases;
suppose c < x;
hence contradiction by A5,A2,XXREAL_1:3;
end;
suppose x <= c;
hence contradiction by A3,A7,XXREAL_1:236;
end;
end;
suppose K is empty;
hence thesis by A1,XXREAL_1:31;
end;
end;
theorem Th5:
for D being non empty set, D1 being non empty Subset of D holds
n-tuples_on D1 c= n-tuples_on D
proof
let D be non empty set, D1 be non empty Subset of D;
n-tuples_on D /\ n-tuples_on D1 = n-tuples_on D1 by MARGREL1:21;
hence thesis by XBOOLE_1:17;
end;
theorem Th6:
for X being non empty set,f being Function st f = Seg n --> X holds
f is non-empty n-element FinSequence
proof
let X be non empty set, f be Function;
assume
A1: f = Seg n --> X;
card f = card dom f by CARD_1:62;
then card f = card Seg n by A1,FUNCOP_1:13;
then card f = card n by FINSEQ_1:55;
hence f is non-empty n-element FinSequence by A1,CARD_1:def 7;
end;
definition
let n be Nat;
func ProductREAL(n) -> non-empty n-element FinSequence equals
Seg n --> REAL;
coherence by Th6;
end;
theorem
ProductREAL(n) = Seg n --> the carrier of R^1;
theorem Th7:
product (Seg n --> REAL) = REAL n
proof
REAL n = Funcs(Seg n,REAL) by FINSEQ_2:93;
hence thesis by CARD_3:11;
end;
theorem
product ProductREAL(n) = REAL n by Th7;
theorem Th8:
for X being set holds product(Seg n --> X) = n-tuples_on X
proof
let X be set;
n-tuples_on X = Funcs(Seg n,X) by FINSEQ_2:93;
hence thesis by CARD_3:11;
end;
theorem Th9:
for D being non empty set, x being Tuple of n, D holds x in Funcs(Seg n,D)
proof
let D be non empty set, x be Tuple of n,D;
x in n-tuples_on D by FINSEQ_2:131;
hence thesis by FINSEQ_2:93;
end;
theorem Th10:
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
proof
let O1 be Subset of TOP-REAL n,O2 be Subset of TopSpaceMetr Euclid n;
assume
A1: O1 = O2;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
hence thesis by A1;
end;
theorem
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
proof
assume
A1: e = p;
A2: for m be non zero Element of NAT holds
OpenHypercube(e,1/m) = OpenHypercube(p,1/m)
proof
let m be non zero Element of NAT;
consider e0 be Point of Euclid n such that
A3: p = e0 and
A4: OpenHypercube(e0,1/m) = OpenHypercube(p,1/m) by TIETZE_2:def 1;
thus thesis by A1,A3,A4;
end;
set XE = the set of all OpenHypercube(e,1/m) where
m is non zero Element of NAT;
set XTR = the set of all OpenHypercube(p,1/m) where
m is non zero Element of NAT;
thus XE c= XTR
proof
let x be object;
assume x in XE;
then consider me be non zero Element of NAT such that
A6: x = OpenHypercube(e,1/me);
x = OpenHypercube(p,1/me) by A6,A2;
hence thesis;
end;
let x be object;
assume x in XTR;
then consider mtr be non zero Element of NAT such that
A7: x = OpenHypercube(p,1/mtr);
x = OpenHypercube(e,1/mtr) by A7,A2;
hence thesis;
end;
theorem Th11:
q in OpenHypercube(p,r) implies p in OpenHypercube(q,r)
proof
assume
A1: q in OpenHypercube(p,r);
now
let i be Nat;
assume i in Seg n;
then q.i in ].p.i - r,p.i + r.[ by A1,TIETZE_2:4;
then p.i - r < q.i & q.i < p.i + r by XXREAL_1:4;
then p.i - r + r < q.i + r & q.i - r < p.i + r - r by XREAL_1:8;
hence p.i in ].q.i - r,q.i + r.[ by XXREAL_1:4;
end;
hence thesis by TIETZE_2:4;
end;
theorem Th12:
q in OpenHypercube(p,r/2) implies OpenHypercube(q,r/2) c= OpenHypercube(p,r)
proof
assume
A1: q in OpenHypercube(p,r/2);
let x be object;
assume
A2: x in OpenHypercube(q,r/2);
then reconsider x1 = x as Point of TOP-REAL n;
now
let i be Nat;
assume
A3: i in Seg n;
then x1.i in ].q.i-r/2,q.i+r/2.[ by A2,TIETZE_2:4; then
A4: q.i-r/2 < x1.i & x1.i < q.i+r/2 by XXREAL_1:4;
q.i in ].p.i-r/2,p.i+r/2.[ by A1,A3,TIETZE_2:4;
then p.i - r/2 < q.i & q.i < p.i + r/2 by XXREAL_1:4;
then p.i - r/2 - r/2 < q.i - r/2 & q.i + r/2 < p.i + r/2 + r/2
by XREAL_1:8;
then p.i - r < x1.i & x1.i < p.i + r by A4,XXREAL_0:2;
hence x1.i in ].p.i-r,p.i+r.[ by XXREAL_1:4;
end;
hence x in OpenHypercube(p,r) by TIETZE_2:4;
end;
definition
let x be Element of [:REAL,REAL:];
redefine func x`1 -> Element of REAL; :: redefines `1 (XTUPLE_0, definition)
coherence
proof
ex a,b be object st a in REAL & b in REAL & x = [a,b] by ZFMISC_1:def 2;
hence thesis;
end;
redefine func x`2 -> Element of REAL; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
ex a,b be object st a in REAL & b in REAL & x = [a,b] by ZFMISC_1:def 2;
hence thesis;
end;
end;
definition
let n be Nat, x be Element of [:REAL n,REAL n:];
redefine func x`1 -> Element of REAL n; :: redefines `1 (XTUPLE_0, definition)
coherence
proof
ex a,b be object st a in REAL n & b in REAL n & x = [a,b]
by ZFMISC_1:def 2;
hence thesis;
end;
redefine func x`2 -> Element of REAL n; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
ex a,b be object st a in REAL n & b in REAL n & x = [a,b]
by ZFMISC_1:def 2;
hence thesis;
end;
end;
theorem Th13:
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
proof
let f be n-element FinSequence of [:REAL,REAL:];
defpred P[Nat,set] means $2 = (f/.$1)`1;
A2: for i be Nat st i in Seg n ex d be Element of REAL st P[i,d];
ex x1 being FinSequence of REAL st len x1 = n & for i be Nat st
i in Seg n
holds P[i,x1/.i] from FINSEQ_4:sch 1(A2);
then consider x1 being FinSequence of REAL such that
A3: len x1 = n and
A4: for i be Nat st i in Seg n holds x1/.i = (f/.i)`1;
dom x1 = Seg n by A3,FINSEQ_1:def 3;
then reconsider x1 as Element of REAL n by REAL_NS1:6;
defpred Q[Nat,set] means $2 = (f/.$1)`2;
A5: for i be Nat st i in Seg n ex d be Element of REAL st Q[i,d];
ex x2 being FinSequence of REAL st len x2 = n & for i be Nat st
i in Seg n
holds Q[i,x2/.i] from FINSEQ_4:sch 1(A5);
then consider x2 being FinSequence of REAL such that
A6: len x2 = n and
A7: for i be Nat st i in Seg n holds x2/.i = (f/.i)`2;
dom x2 = Seg n by A6,FINSEQ_1:def 3;
then reconsider x2 as Element of REAL n by REAL_NS1:6;
reconsider x = [x1,x2] as Element of [:REAL n,REAL n:] by ZFMISC_1:def 2;
take x;
now
let i be Nat;
assume
A8: i in Seg n; then
A9: x1/.i = (f/.i)`1 & x2/.i = (f/.i)`2 by A4,A7;
i in dom x1 & i in dom x2 by A3,FINSEQ_1:def 3,A8,A6;
hence (x`1).i = (f/.i)`1 & (x`2).i = (f/.i)`2 by A9,PARTFUN1:def 6;
end;
hence thesis;
end;
begin :: The set of n-tuples of rational numbers
definition
let n;
func RAT n -> FinSequenceSet of RAT equals n-tuples_on RAT;
coherence;
end;
theorem Th14:
RAT 0 = {0}
proof
RAT 0 = {<*>RAT} by FINSEQ_2:94
.= {{}};
hence thesis;
end;
registration
cluster RAT 0 -> trivial;
coherence by Th14;
end;
registration
let n;
cluster RAT n -> non empty;
coherence;
end;
registration
let n;
cluster -> n-element for Element of RAT n;
coherence;
end;
registration
let n;
cluster RAT n -> countable;
coherence by CARD_4:10;
end;
registration
let n be positive Nat;
cluster RAT n -> infinite;
correctness
proof
deffunc F(Element of n-tuples_on RAT) = $1.1;
consider f be Function such that
A1: dom f = n-tuples_on RAT &
for d be Element of n-tuples_on RAT holds f.d = F(d) from FUNCT_1:sch 4;
for y being object holds y in f.:(n-tuples_on RAT) iff y in RAT
proof
let y be object;
0+1 < n+1 by XREAL_1:6; then
A2: 1 <= n by NAT_1:13; then
A3: 1 in Seg n;
hereby
assume y in f.:(n-tuples_on RAT);
then consider x be object such that
A4: x in dom f & x in n-tuples_on RAT & y = f.x by FUNCT_1:def 6;
reconsider x as Element of n-tuples_on RAT by A4;
A5: y = x.1 by A1,A4;
x in Funcs(Seg n,RAT) by A4,FINSEQ_2:93;
then consider f1 being Function such that
A6: x = f1 & dom f1 = Seg n & rng f1 c= RAT by FUNCT_2:def 2;
thus y in RAT by A3,A5,A6,FUNCT_1:3;
end;
assume y in RAT; then
A7: {y} c= RAT by ZFMISC_1:31;
set x = Seg n --> y;
A8: dom x = Seg n & rng x c= {y} by FUNCOP_1:13;
rng x c= RAT by A7;
then x in Funcs(Seg n,RAT) by A8,FUNCT_2:def 2;
then reconsider x as Element of n-tuples_on RAT by FINSEQ_2:93;
f.x = x.1 by A1 .= y by A2,FINSEQ_1:1,FUNCOP_1:7;
hence y in f.:(n-tuples_on RAT) by A1,FUNCT_1:def 6;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let n be positive Nat;
cluster RAT n -> denumerable;
coherence;
end;
theorem Th15:
RAT n is dense Subset of TOP-REAL n
proof
RAT n is Subset of REAL n by NUMBERS:12,Th5;
then reconsider RATN = RAT n as Subset of TOP-REAL n by EUCLID:22;
for Q be Subset of TOP-REAL n st Q <> {} & Q is open holds RATN meets Q
proof
let Q be Subset of TOP-REAL n;
assume that
A1: Q <> {} and
A2: Q is open;
consider q be object such that
A3: q in Q by A1,XBOOLE_0:def 1;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider Q0=Q as Subset of TopSpaceMetr Euclid n;
reconsider q0 = q as Point of Euclid n by A3,EUCLID:67;
Q0 is open by A2,Th10;
then consider m being non zero Element of NAT such that
A6: OpenHypercube(q0,1/m) c= Q0 by A3,EUCLID_9:23;
set OH = OpenHypercube(q0,1/m), f = Intervals(q0,1/m);
A7: dom f = dom q0 by EUCLID_9:def 3;
A8: for x be object st x in dom f holds ex k be Element of RAT st k in f.x
proof
let x be object;
assume
A9: x in dom f;
reconsider FF = ].q0.x - (1/m),q0.x + (1/m).[ as open Subset of R^1
by BORSUK_5:39;
A10: q0.x - (1/m) < q0.x by XREAL_1:44;
q0.x < q0.x + (1/m) by XREAL_1:29;
then q0.x - (1/m) < q0.x + (1/m) by A10,XXREAL_0:2;
then FF <> {} & FF is open by XXREAL_1:33;
then FF meets RAT by TOPGEN_1:51,TOPS_1:45;
then consider k be object such that
A11: k in FF & k in RAT by XBOOLE_0:3;
take k;
thus thesis by A11,A9,A7,EUCLID_9:def 3;
end;
q in TOP-REAL n by A3;
then q in REAL n by EUCLID:22;
then reconsider q1 = q as FinSequence of REAL by FINSEQ_2:131;
A12: dom q1 = Seg n by A3,FINSEQ_1:89;
defpred P[object,object] means $2 in f.$1 & $2 is Element of RAT;
A13: for x be Nat st x in Seg n ex y be object st P[x,y]
proof
let x be Nat;
assume x in Seg n;
then consider k be Element of RAT such that
A14: k in f.x by A8,A7,A12;
take k;
thus thesis by A14;
end;
consider p be FinSequence such that
A15: dom p = Seg n and
A16: for k be Nat st k in Seg n holds P[k,p.k] from FINSEQ_1:sch 1(A13);
A17: p is n-element
proof
Seg len p = dom p by FINSEQ_1:def 3;
hence thesis by A15,FINSEQ_1:6,CARD_1:def 7;
end;
p is Tuple of n,RAT
proof
p is FinSequence of RAT
proof
rng p c= RAT
proof
let x be object;
assume x in rng p;
then consider x0 be object such that
A18: x0 in dom p and
A19: x = p.x0 by FUNCT_1:def 3;
p.x0 in f.x0 & p.x0 is Element of RAT by A16,A18,A15;
hence x in RAT by A19;
end;
hence thesis by FINSEQ_1:def 4;
end;
hence thesis by A17;
end;
then
A20: p in RAT n by FINSEQ_2:131;
p in OH
proof
p in product Intervals(q0,1/m)
proof
now
let x be object;
assume x in dom f;
then x in Seg n by A7,FINSEQ_1:89;
hence p.x in f.x by A16;
end;
hence thesis by A15,A7,A12,CARD_3:9;
end;
hence thesis;
end;
hence thesis by A6,A20,XBOOLE_0:3;
end;
hence thesis by TOPS_1:45;
end;
registration
let n;
cluster RAT n -> countable dense for Subset of TOP-REAL n;
coherence by Th15;
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;
existence by TOPGEN_4:57;
end;
begin :: A countable base of an n-dimensional Euclidean space (Version 2)
registration
let n,e;
cluster OpenHypercubes(e) -> countable;
coherence
proof
set OH = OpenHypercubes(e);
deffunc F(Nat) = OpenHypercube(e,1/$1);
defpred P[Nat] means $1 <> 0;
A1: {F(n) where n is Nat:P[n]} is countable from CARD_4:sch 1;
{F(n) where n is Nat:P[n]} = OH
proof
thus {F(n) where n is Nat:P[n]} c= OH
proof
let x be object;
assume x in {F(n) where n is Nat:P[n]};
then consider n0 be Nat such that
A3: x = F(n0) and
A4: P[n0];
n0 is non zero Element of NAT by A4,ORDINAL1:def 12;
hence x in OH by A3;
end;
let x be object;
assume x in OH;
then consider m0 be non zero Element of NAT such that
A5: x = OpenHypercube(e,1/m0);
thus thesis by A5;
end;
hence thesis by A1;
end;
end;
definition
let n;
func OpenHypercubesRAT(n) -> non empty set equals
{OpenHypercubes(q) where q is Point of Euclid n : q in RAT n};
coherence
proof
consider q be object such that
A1: q in RAT n by XBOOLE_0:def 1;
RAT n c= REAL n by NUMBERS:12,Th5;
then reconsider q1 = q as Point of Euclid n by A1;
OpenHypercubes(q1) in {OpenHypercubes(q) where q is Point of Euclid n :
q in RAT n} by A1;
hence thesis;
end;
end;
definition
let n;
let q be Element of RAT n;
func @q -> Point of Euclid n equals q;
coherence
proof
RAT n c= REAL n & q in RAT n by NUMBERS:12,Th5;
hence thesis;
end;
end;
definition
let n;
let q be object such that
A1: q in RAT n;
func object2RAT(q,n) -> Element of RAT n equals :Def1:
q;
coherence by A1;
end;
Th16:
OpenHypercubesRAT(n) is countable
proof
deffunc F2(object) = OpenHypercubes(@object2RAT($1,n));
consider ff be Function such that
A1: dom ff = RAT n and
A2: for x be object st x in RAT n holds ff.x = F2(x) from FUNCT_1:sch 3;
A3: OpenHypercubesRAT(n) = rng ff
proof
hereby
let x be object;
assume x in OpenHypercubesRAT(n);
then consider q0 be Point of Euclid n such that
A4: x = OpenHypercubes(q0) and
A5: q0 in RAT n;
x = ff.q0
proof
ff.q0 = F2(q0) by A5,A2;
hence thesis by A4,A5,Def1;
end;
hence x in rng ff by A5,A1,FUNCT_1:def 3;
end;
let x be object;
assume x in rng ff;
then consider q0 be object such that
A6: q0 in dom ff and
A7: x = ff.q0 by FUNCT_1:def 3;
RAT n c= REAL n & q0 in RAT n by NUMBERS:12,Th5,A6,A1;
then reconsider q1 = q0 as Point of Euclid n;
ff.q1 = F2(q0) by A6,A1,A2;
hence x in OpenHypercubesRAT(n) by A7;
end;
card rng ff c= card dom ff by CARD_2:61;
hence thesis by A3,A1,WAYBEL12:1;
end;
registration let n;
cluster OpenHypercubesRAT(n) -> countable;
coherence by Th16;
end;
Th17:
union OpenHypercubesRAT(n) is countable
proof
for Y be set st Y in OpenHypercubesRAT(n) holds Y is countable
proof
let Y be set such that
A2: Y in OpenHypercubesRAT(n);
consider q0 be Point of Euclid n such that
A3: Y = OpenHypercubes(q0) and
q0 in RAT n by A2;
thus thesis by A3;
end;
hence thesis by CARD_4:12;
end;
registration let n;
cluster union OpenHypercubesRAT(n) -> countable;
coherence by Th17;
end;
Th18:
union OpenHypercubesRAT(n) is Subset-Family of TOP-REAL n
proof
union OpenHypercubesRAT(n) c= bool the carrier of TOP-REAL n
proof
let x be object;
assume x in union OpenHypercubesRAT(n);
then consider y be set such that
A1: x in y and
A2: y in OpenHypercubesRAT(n) by TARSKI:def 4;
consider q0 be Point of Euclid n such that
A3: y = OpenHypercubes(q0) and
q0 in RAT n by A2;
x in bool REAL n by A1,A3;
hence thesis by EUCLID:22;
end;
hence thesis;
end;
theorem Th19:
union OpenHypercubesRAT(n) is open Subset-Family of TOP-REAL n
proof
reconsider UO = union OpenHypercubesRAT(n) as Subset-Family of TOP-REAL n
by Th18;
UO is open
proof
let P be Subset of TOP-REAL n;
assume P in UO;
then consider X be set such that
A1: P in X and
A2: X in OpenHypercubesRAT(n) by TARSKI:def 4;
consider q0 be Point of Euclid n such that
A3: X = OpenHypercubes(q0) and
q0 in RAT n by A2;
A4: OpenHypercubes(q0) is open;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider P0=P as Subset of TopSpaceMetr Euclid n;
P0 is open by A4,A3,A1;
hence thesis by Th10;
end;
hence thesis;
end;
theorem Th20:
for O being non empty open Subset of TOP-REAL n holds
ex p being Element of RAT n st p in O
proof
let O be non empty open Subset of TOP-REAL n;
RAT n is dense Subset of TOP-REAL n by Th15;
then O meets RAT n by TOPS_1:45;
then consider x be object such that
A1: x in O and
A2: x in RAT n by XBOOLE_0:3;
reconsider x as Element of RAT n by A2;
take x;
thus thesis by A1;
end;
theorem Th21:
for cB being Subset-Family of TOP-REAL n st
cB = union OpenHypercubesRAT(n) holds cB is quasi_basis
proof
let F be Subset-Family of TOP-REAL n;
assume
A1: F = union OpenHypercubesRAT(n);
F is quasi_basis
proof
now
let x be object;
assume
A2: x in the topology of TOP-REAL n;
then reconsider x1=x as Subset of TOP-REAL n;
A3: x1 is open by A2;
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
then reconsider x2=x1 as Subset of TopSpaceMetr Euclid n;
A4: x2 is open by A3,Th10;
set Y = {t where t is Subset of TOP-REAL n: t in F & t c= x1};
A5: Y is Subset-Family of TOP-REAL n
proof
Y c= bool the carrier of TOP-REAL n
proof
let t be object;
assume t in Y;
then consider t0 be Subset of TOP-REAL n such that
A6: t=t0 and
t0 in F and
t0 c= x1;
thus t in bool the carrier of TOP-REAL n by A6;
end;
hence thesis;
end;
A7: Y c= F
proof
let t be object;
assume t in Y;
then consider t0 be Subset of TOP-REAL n such that
A8: t=t0 and
A9: t0 in F and
t0 c= x1;
thus t in F by A8,A9;
end;
x = union Y
proof
reconsider x3=x as set by TARSKI:1;
A10: x3 c= union Y
proof
let t be object;
assume
A11: t in x3;
then t in x2;
then reconsider t1 = t as Point of Euclid n;
consider m1 being non zero Element of NAT such that
A12: OpenHypercube(t1,1/m1) c= x2 by A4,A11,EUCLID_9:23;
reconsider t2 = t1 as Point of TOP-REAL n by EUCLID:67;
reconsider Invm1Div2 = 1/m1/2 as positive Real;
consider e be Point of Euclid n such that
t2 = e and
A13: OpenHypercube(t2,1/m1/2) = OpenHypercube(e,1/m1/2)
by TIETZE_2:def 1;
consider q0 be Element of RAT n such that
A14: q0 in OpenHypercube(t2,Invm1Div2) by A13,Th20;
q0 in RAT n & RAT n is Subset of REAL n by NUMBERS:12,Th5;
then reconsider q1 = q0 as Point of TOP-REAL n by EUCLID:22;
reconsider r = Invm1Div2 * 2 as Real;
A15: OpenHypercube(q1,r/2) c= OpenHypercube(t2,r) by A14,Th12;
reconsider q2 = q1 as Point of Euclid n by EUCLID:67;
set OO = OpenHypercube(q2,Invm1Div2);
A16: now
thus OpenHypercube(t2,r) = OpenHypercube(t2,1/m1);
consider ez be Point of Euclid n such that
A17: t2 = ez and
A18: OpenHypercube(t2,1/m1) = OpenHypercube(ez,1/m1)
by TIETZE_2:def 1;
thus OpenHypercube(t1,1/m1) = OpenHypercube(t2,1/m1) by A17,A18;
thus OpenHypercube(t1,1/m1) c= x1 by A12;
end;
consider er be Point of Euclid n such that
A19: q2 = er and
A20: OpenHypercube(q1,Invm1Div2) = OpenHypercube(er,Invm1Div2)
by TIETZE_2:def 1;
A21: Invm1Div2 = 1 / ( m1 * 2 ) by XCMPLX_1:78;
A22: OO in union OpenHypercubesRAT(n)
proof
consider e be Point of Euclid n such that
A23: q2 = e and
OpenHypercube(q2,Invm1Div2) = OpenHypercube(e,Invm1Div2);
A24: OO in OpenHypercubes(e) by A21,A23;
OpenHypercubes(e) in OpenHypercubesRAT(n) by A23;
hence thesis by A24,TARSKI:def 4;
end;
t in OO & OO in F & OO c= x1
by A22,A1,A19,A20,A14,Th11,A15,A16;
then t in OO & OO in Y;
hence t in union Y by TARSKI:def 4;
end;
union Y c= x1
proof
let t be object;
assume t in union Y;
then consider Z be set such that
A25: t in Z and
A26: Z in Y by TARSKI:def 4;
consider t0 be Subset of TOP-REAL n such that
A27: Z = t0 and
t0 in F and
A28: t0 c= x1 by A26;
thus t in x1 by A25,A27,A28;
end;
then x1 = union Y by A10;
hence thesis;
end;
hence x in UniCl F by A5,A7,CANTOR_1:def 1;
end;
then the topology of TOP-REAL n c= UniCl F;
hence thesis by CANTOR_1:def 2;
end;
hence thesis;
end;
Th22:
union OpenHypercubesRAT(n) is non empty
proof
assume union OpenHypercubesRAT(n) is empty;
then
A1: OpenHypercubesRAT(n) = {{}} by SCMYCIEL:18;
OpenHypercubesRAT(n) is non empty;
then consider x be object such that
A2: x in OpenHypercubesRAT(n);
consider q be Point of Euclid n such that
A3: x = OpenHypercubes(q) and
q in RAT n by A2;
thus contradiction by A3,A1,A2,TARSKI:def 1;
end;
registration let n;
cluster union OpenHypercubesRAT(n) -> non empty;
coherence by Th22;
end;
definition
let n;
func dense_countable_OpenHypercubes(n) -> countable open
Subset-Family of TOP-REAL n equals union OpenHypercubesRAT(n);
coherence by Th19;
end;
theorem
dense_countable_OpenHypercubes(n) =
{OpenHypercube(q,1/m) where q is Point of Euclid n,
m is positive Nat:q in RAT n}
proof
now
let x be object;
hereby
assume x in dense_countable_OpenHypercubes(n);
then consider y be set such that
A1: x in y and
A2: y in OpenHypercubesRAT(n) by TARSKI:def 4;
consider z be Point of Euclid n such that
A3: y = OpenHypercubes(z) and
A4: z in RAT n by A2;
consider m be non zero Element of NAT such that
A5: x = OpenHypercube(z,1/m) by A1,A3;
thus x in {OpenHypercube(q,1/m) where q is Point of Euclid n,
m is positive Nat:q in RAT n} by A4,A5;
end;
assume x in {OpenHypercube(q,1/m) where q is Point of Euclid n,
m is positive Nat:q in RAT n};
then consider q0 be Point of Euclid n, m0 be positive Nat such that
A6: x = OpenHypercube(q0,1/m0) and
A7: q0 in RAT n;
reconsider p = q0 as Point of Euclid n;
reconsider m1 = m0 as non zero Element of NAT by ORDINAL1:def 12;
OpenHypercube(q0,1/m0) = OpenHypercube(q0,1/m1);
then x in OpenHypercubes(p) & OpenHypercubes(p) in OpenHypercubesRAT(n)
by A6,A7;
hence x in dense_countable_OpenHypercubes(n) by TARSKI:def 4;
end;
hence thesis by TARSKI:2;
end;
registration :: Second version
let n be Nat;
cluster countable for Basis of TOP-REAL n;
existence
proof
dense_countable_OpenHypercubes(n) is Basis of TOP-REAL n &
dense_countable_OpenHypercubes(n) is countable by Th21;
hence thesis;
end;
end;
theorem
dense_countable_OpenHypercubes(n) is countable Basis of TOP-REAL n
by Th21;
theorem Th23:
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
proof
let O be open Subset of TOP-REAL n;
the topology of TOP-REAL n c= UniCl dense_countable_OpenHypercubes(n)
by Th21,CANTOR_1:def 2;
then O in UniCl dense_countable_OpenHypercubes(n) by PRE_TOPC:def 2;
then consider Y be Subset-Family of TOP-REAL n such that
A1: Y c= dense_countable_OpenHypercubes(n) and
A2: O = union Y by CANTOR_1:def 1;
thus thesis by A1,A2;
end;
theorem Th24:
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
proof
let O be open non empty Subset of TOP-REAL n;
consider Y be Subset of dense_countable_OpenHypercubes(n) such that
Y is countable and
A1: O = union Y by Th23;
take Y;
thus Y is non empty by A1,ZFMISC_1:2;
thus O = union Y by A1;
consider g be Function of omega,Y such that
A2: rng g = Y by A1,ZFMISC_1:2,CARD_3:96;
take g;
A3: dom g = omega by A1,ZFMISC_1:2,FUNCT_2:def 1;
O = Union g by A1,A2;
hence thesis by A3,CARD_5:2;
end;
theorem Th25:
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
proof
let O be open non empty Subset of TOP-REAL n;
consider Y being Subset of dense_countable_OpenHypercubes(n) such that
Y is non empty and
A1: O = union Y and
A2: 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 by Th24;
consider g be Function of NAT,Y such that
A3: for x being object holds x in O iff ex y being object st y in NAT &
x in g.y by A2;
reconsider g2 = g as sequence of dense_countable_OpenHypercubes(n)
by A1,ZFMISC_1:2,FUNCT_2:7;
for x being object holds x in O iff ex y being object st y in NAT &
x in g2.y by A3;
hence thesis;
end;
theorem
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
proof
let O be open non empty Subset of TOP-REAL n;
consider s being sequence of dense_countable_OpenHypercubes(n) such that
A1: for x being object holds x in O iff ex y being object st y in NAT &
x in s.y by Th25;
A2: dom s = NAT by FUNCT_2:def 1;
take s;
now
let x be object;
hereby
assume x in O;
then consider y be object such that
A3: y in NAT and
A4: x in s.y by A1;
s.y in rng s by A3,A2,FUNCT_1:def 3;
hence x in Union s by A4,TARSKI:def 4;
end;
assume x in Union s;
then consider y be set such that
A5: x in y and
A6: y in rng s by TARSKI:def 4;
consider z be object such that
A7: z in dom s and
A8: y = s.z by A6,FUNCT_1:def 3;
thus x in O by A1,A5,A7,A8;
end;
hence thesis by TARSKI:2;
end;
begin :: The set of all left open real bounded intervals
definition
func the_set_of_all_left_open_real_bounded_intervals
-> Subset-Family of REAL equals
the set of all ].a,b.] where a,b is Real;
coherence
proof
the set of all ].a,b.] where a,b is Real c= bool REAL
proof
let x be object;
assume x in the set of all ].a,b.] where a,b is Real;
then ex a0,b0 be Real st x = ].a0,b0.];
hence thesis;
end;
hence thesis;
end;
end;
registration
cluster the_set_of_all_left_open_real_bounded_intervals -> non empty;
coherence
proof
]. 0 , 0 .] in the_set_of_all_left_open_real_bounded_intervals;
hence thesis;
end;
end;
theorem
the_set_of_all_left_open_real_bounded_intervals c=
{ I where I is Subset of REAL: I is left_open_interval}
proof
let x be object;
assume x in the_set_of_all_left_open_real_bounded_intervals;
then consider a,b be Real such that
A1: x = ].a,b.];
reconsider x1=x as Subset of REAL by A1;
reconsider a as R_eal by XREAL_0:def 1,NUMBERS:31;
x1 = ].a,b.] by A1;
then x1 is left_open_interval by MEASURE5:def 5;
hence thesis;
end;
theorem Th26:
the_set_of_all_left_open_real_bounded_intervals is
cap-closed diff-finite-partition-closed with_empty_element
with_countable_Cover
proof
the_set_of_all_left_open_real_bounded_intervals =
{].a,b.] where a,b is Real:a <= b}
proof
hereby
let x be object;
assume x in the_set_of_all_left_open_real_bounded_intervals;
then consider a,b be Real such that
A1: x = ].a,b.];
per cases;
suppose a <= b;
hence x in {].a,b.] where a,b is Real:a <= b} by A1;
end;
suppose not a <= b;
then x = ]. 0 , 0 .] by A1,XXREAL_1:26;
hence x in {].a,b.] where a,b is Real:a <= b};
end;
end;
let x be object;
assume x in {].a,b.] where a,b is Real:a <= b};
then ex a,b be Real st x = ].a,b.] & a <= b;
hence x in the_set_of_all_left_open_real_bounded_intervals;
end;
hence thesis by SRINGS_2:9;
end;
theorem
the_set_of_all_left_open_real_bounded_intervals is Semiring of REAL
by Th26,SRINGS_3:10;
begin :: The set of all right open real bounded intervals
definition
func the_set_of_all_right_open_real_bounded_intervals
-> Subset-Family of REAL equals
the set of all [.a,b.[ where a,b is Real;
coherence
proof
the set of all [.a,b.[ where a,b is Real c= bool REAL
proof
let x be object;
assume x in the set of all [.a,b.[ where a,b is Real;
then ex a0,b0 be Real st x = [.a0,b0.[;
hence thesis;
end;
hence thesis;
end;
end;
registration
cluster the_set_of_all_right_open_real_bounded_intervals ->
non empty;
coherence
proof
[.0,0.[ in the_set_of_all_right_open_real_bounded_intervals;
hence thesis;
end;
end;
theorem Th27:
the_set_of_all_right_open_real_bounded_intervals c=
{ I where I is Subset of REAL: I is right_open_interval}
proof
let x be object;
assume x in the_set_of_all_right_open_real_bounded_intervals;
then consider a,b be Real such that
A1: x = [.a,b.[;
reconsider x1=x as Subset of REAL by A1;
reconsider b as R_eal by XREAL_0:def 1,NUMBERS:31;
x1 = [.a,b.[ by A1;
then x1 is right_open_interval by MEASURE5:def 4;
hence thesis;
end;
Th28:
the_set_of_all_right_open_real_bounded_intervals is with_empty_element
proof
[. 0 , 0 .[ in the_set_of_all_right_open_real_bounded_intervals &
[. 0 , 0 .[ = {};
hence thesis;
end;
Th29:
the_set_of_all_right_open_real_bounded_intervals is cap-closed
diff-finite-partition-closed with_empty_element
proof
{ I where I is Subset of REAL: I is right_open_interval } c= bool REAL
proof
let x be object;
assume x in { I where I is Subset of REAL: I is right_open_interval };
then consider I be Subset of REAL such that
A1: x = I and I is right_open_interval;
thus thesis by A1;
end;
then reconsider S = { I where I is Subset of REAL:
I is right_open_interval } as Subset-Family of REAL;
A2: S is cap-closed by SRINGS_3:27;
now
let A,B be set;
assume
A3: A in the_set_of_all_right_open_real_bounded_intervals &
B in the_set_of_all_right_open_real_bounded_intervals; then
A4: A in S & B in S by Th27;
then consider I be Subset of REAL such that
A5: A = I & I is right_open_interval;
consider J be Subset of REAL such that
A6: B = J & J is right_open_interval by A4;
S is cap-closed & I in S & J in S by A5,A6,SRINGS_3:27;
then I /\ J in S by FINSUB_1:def 2;
then consider K be Subset of REAL such that
A7: I /\ J = K and
A8: K is right_open_interval;
consider a be Real,b be R_eal such that
A9: K = [.a,b.[ by A8,MEASURE5:def 4;
per cases;
suppose
A10: K is non empty;
consider x be object such that
A11: x in K by A10;
reconsider x as Real by A11;
b is Real
proof
assume not b is Real;
then not b in REAL & a in REAL & a <= b
by XREAL_0:def 1,A10,A9,XXREAL_1:27;
then
A12: b = +infty by XXREAL_0:10;
a <= x by A11,A9,XXREAL_1:3; then
A13: [.x,+infty.[ c= A & [.x,+infty.[ c= B
by A9,A12,XXREAL_1:38,A5,A6,A7,XBOOLE_1:18;
consider xa,xb be Real such that
A14: A = [.xa,xb.[ by A3;
A15: not xb in A by A14,XXREAL_1:3;
per cases;
suppose xb < x; then
A16: not x in A by A14,XXREAL_1:3;
x < b by A11,A9,XXREAL_1:3;
hence contradiction by A16,A13,A12,XXREAL_1:3;
end;
suppose x <= xb;
hence contradiction by A15,A13,XXREAL_1:236;
end;
end;
then reconsider b as Real;
K = [.a,b.[ by A9;
hence A /\ B in the_set_of_all_right_open_real_bounded_intervals
by A7,A5,A6;
end;
suppose K is empty;
hence A /\ B in the_set_of_all_right_open_real_bounded_intervals
by A7,A5,A6,Th28,SETFAM_1:def 8;
end;
end;
hence the_set_of_all_right_open_real_bounded_intervals is cap-closed
by FINSUB_1:def 2;
now
let A,B be Element of the_set_of_all_right_open_real_bounded_intervals;
assume
A17: A\B is non empty;
A18: A in S & B in S by Th27;
then consider I be Subset of REAL such that
A19: A = I and I is right_open_interval;
consider J be Subset of REAL such that
A20: B = J and J is right_open_interval by A18;
S is semi-diff-closed & S is non empty by SRINGS_3:27;
then S is diff-c=-finite-partition-closed by SRINGS_3:9;
then S is diff-finite-partition-closed & I is Element of S &
J is Element of S & I\J is non empty by A17,A19,A20,A2,Th27;
then consider x be finite Subset of S such that
A21: x is a_partition of I \ J by SRINGS_1:def 2;
now
x in bool the_set_of_all_right_open_real_bounded_intervals
proof
reconsider x1=x as set;
x1 c= the_set_of_all_right_open_real_bounded_intervals
proof
let t be object;
assume
A22: t in x1;
then t in S;
then consider K be Subset of REAL such that
A23: t = K and
A24: K is right_open_interval;
per cases;
suppose K is empty;
hence thesis by A23,Th28,SETFAM_1:def 8;
end;
suppose
A25: K is non empty;
consider a be Real, b be R_eal such that
A26: K = [.a,b.[ by A24,MEASURE5:def 4;
A27: K c= A \ B & A \ B c= A by A22,A23,A21,A19,A20,XBOOLE_1:36;
A in the_set_of_all_right_open_real_bounded_intervals;
then consider e,c be Real such that
A28: A = [.e,c.[;
now
thus a is Real & c is Real;
thus b is R_eal;
thus a < b by A25,A26,XXREAL_1:27;
now
let x be object;
assume
A29: x in [.a,b.[; then
A30: x in [.e,c.[ by A26,A27,A28;
reconsider x1 = x as ExtReal by A29;
a <= x1 & x1 < b & e <= x1 & x1 < c by A29,A30,XXREAL_1:3;
hence x in [.a,c.[ by XXREAL_1:3;
end;
hence [.a,b.[ c= [.a,c.[;
end;
then b is Real by Th4;
hence thesis by A26,A23;
end;
end;
hence thesis;
end;
hence x is finite Subset of
the_set_of_all_right_open_real_bounded_intervals;
reconsider x1 = x as Subset-Family of A \ B by A21,A19,A20;
thus x is a_partition of A \ B by A19,A20,A21;
end;
hence ex x be finite Subset of
the_set_of_all_right_open_real_bounded_intervals st
x is a_partition of A\B;
end;
hence the_set_of_all_right_open_real_bounded_intervals is
diff-finite-partition-closed with_empty_element
by SRINGS_1:def 2,Th28;
end;
Th30:
the_set_of_all_right_open_real_bounded_intervals is with_countable_Cover
proof
defpred F[object,object] means
$1 is Element of NAT &
$2 in the_set_of_all_right_open_real_bounded_intervals &
ex x be real number st x=$1 & $2=[.-x,x.[;
A1: for x be object st x in NAT holds ex y be object st
y in the_set_of_all_right_open_real_bounded_intervals & F[x,y]
proof
let x be object;
assume
A2: x in NAT;
then reconsider x as real number;
set y = [.-x,x.[;
y in the_set_of_all_right_open_real_bounded_intervals & F[x,y] by A2;
hence thesis;
end;
consider f be Function such that
A3: dom f=NAT & rng f c= the_set_of_all_right_open_real_bounded_intervals and
A4: for x be object st x in NAT holds
F[x,f.x] from FUNCT_1:sch 6(A1);
A5: rng f is Subset-Family of REAL by A3,XBOOLE_1:1;
A6: rng f is countable
proof
reconsider f as SetSequence of REAL by A3,A5,RELSET_1:4,FUNCT_2:def 1;
rng f is countable by TOPGEN_4:58;
hence thesis;
end;
rng f is Cover of REAL
proof
Union f=REAL
proof
thus Union f c= REAL
proof
let x be object;
assume x in Union f;
then consider t be object such that
A7: t in dom f & x in f.t by CARD_5:2;
consider x0 be real number such that
A8: x0=t & f.t=[.-x0,x0.[ by A3,A4,A7;
thus thesis by A7,A8;
end;
for x be object st x in REAL holds x in Union f
proof
let x be object;
assume x in REAL;
then reconsider x as Real;
consider n be Element of NAT such that
A9: |.x.| <= n by MESFUNC1:8;
x in f.(n+1)
proof
consider z be real number such that
A10: z=(n+1) & f.(n+1)=[.-z,z.[ by A4;
A11: x < n+1
proof
assume
A12: not x < n+1;
x <= n by A9,ABSVALUE:def 1;
then n+1 <= n by A12,XXREAL_0:2;
hence contradiction by NAT_1:13;
end;
-(n+1) <= x
proof
per cases;
suppose 0<=x;
hence thesis;
end;
suppose x<0;
then - x <= n by A9,ABSVALUE:def 1;
then - n <= --x by XREAL_1:24; then
A13: -n-1 <= x-1 by XREAL_1:13;
x-1<=x-0 by XREAL_1:13;
hence thesis by A13,XXREAL_0:2;
end;
end;
hence thesis by A10,A11,XXREAL_1:3;
end;
then x in f.(n+1) & f.(n+1) in rng f by A3,FUNCT_1:def 3;
hence thesis by TARSKI:def 4;
end;
hence thesis;
end;
hence thesis by A5,SETFAM_1:45;
end;
hence thesis by A3,A6,SRINGS_1:def 4;
end;
registration
cluster the_set_of_all_right_open_real_bounded_intervals -> cap-closed
diff-finite-partition-closed with_empty_element with_countable_Cover;
coherence by Th29,Th30;
end;
theorem
the_set_of_all_right_open_real_bounded_intervals is Semiring of REAL
by SRINGS_3:10;
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
Seg n --> the_set_of_all_left_open_real_bounded_intervals;
coherence
proof
reconsider S = Seg n --> the_set_of_all_left_open_real_bounded_intervals
as n-element FinSequence by Th6;
for i being Nat st i in Seg n holds S.i is with_empty_element
semi-diff-closed cap-closed Subset-Family of (ProductREAL(n)).i
proof
let i be Nat;
assume
A1: i in Seg n; then
A2: S.i = the_set_of_all_left_open_real_bounded_intervals &
(ProductREAL(n)).i = REAL by FUNCOP_1:7;
reconsider Si = S.i as Subset-Family of REAL by A1,FUNCOP_1:7;
thus thesis by A2,Th26,SRINGS_3:10;
end;
hence thesis by SRINGS_4:def 6;
end;
end;
theorem
ProductLeftOpenIntervals(n) = Seg n --> the set of all ].a,b.] where
a,b is Real;
theorem Th30:
MeasurableRectangle(ProductLeftOpenIntervals(n)) is Semiring of REAL n
proof
MeasurableRectangle(ProductLeftOpenIntervals(n)) is Semiring of
product ProductREAL(n) by SRINGS_4:40;
hence thesis by Th7;
end;
theorem
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
let x be object;
assume
A1: x in MeasurableRectangle(ProductLeftOpenIntervals(n));
MeasurableRectangle(ProductLeftOpenIntervals(n)) is
Subset-Family of REAL n by Th30;
then reconsider y = x as Subset of REAL n by A1;
reconsider x0 = x as set by TARSKI:1;
consider g be Function such that
A2: x = product g and
A3: g in product ProductLeftOpenIntervals(n) by A1,SRINGS_4:def 4;
dom ProductLeftOpenIntervals(n) = Seg n by FUNCOP_1:13; then
A4: dom g = Seg n by A3,CARD_3:9;
take y;
thus x = y;
now
let i be Nat;
assume
A5: i in Seg n;
then i in dom ProductLeftOpenIntervals(n) by FUNCOP_1:13;
then g.i in (ProductLeftOpenIntervals(n)).i by A3,CARD_3:9;
then g.i in the set of all ].a,b.] where a,b is Real by A5,FUNCOP_1:7;
then consider a,b be Real such that
A6: g.i = ].a,b.];
hereby
take a,b;
now
let t be Element of REAL n;
assume t in y;
then consider j0 be Function such that
A7: t=j0 and
dom j0 = Seg n and
A8: for u be object st u in Seg n holds j0.u in g.u
by A2,CARD_3:def 5,A4;
thus t.i in ].a,b.] by A7,A6,A8,A5;
end;
hence ex a,b being Real st
for t be Element of REAL n st t in y holds t.i in ].a,b.];
end;
hence ex a,b being Real st
for t be Element of REAL n st t in y holds t.i in ].a,b.];
end;
hence thesis;
end;
theorem Th31:
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.])
proof
let x be object;
assume
A1: x in MeasurableRectangle(ProductLeftOpenIntervals(n));
MeasurableRectangle(ProductLeftOpenIntervals(n)) is
Subset-Family of REAL n by Th30;
then reconsider y = x as Subset of REAL n by A1;
take y;
reconsider x0 = x as set by TARSKI:1;
consider g be Function such that
A2: x = product g and
A3: g in product ProductLeftOpenIntervals(n) by A1,SRINGS_4:def 4;
dom ProductLeftOpenIntervals(n) = Seg n by FUNCOP_1:13; then
A4: dom g = Seg n by A3,CARD_3:9;
A5: now
let i be Nat;
assume
A6: i in Seg n;
then i in dom ProductLeftOpenIntervals(n) by FUNCOP_1:13;
then g.i in (ProductLeftOpenIntervals(n)).i by A3,CARD_3:9;
then g.i in the_set_of_all_left_open_real_bounded_intervals
by A6,FUNCOP_1:7;
hence ex a,b be Real st g.i = ].a,b.];
end;
defpred P[Nat,set] means ex x be Element of [:REAL,REAL:] st $2 = x &
g.$1 = ].x`1,x`2.];
A7: for i be Nat st i in Seg n holds ex d be Element of [:REAL,REAL:] st P[i,d]
proof
let i be Nat;
assume i in Seg n;
then consider a,b be Real such that
A8: g.i = ].a,b.] by A5;
set d = [a,b];
a in REAL & b in REAL by XREAL_0:def 1;
then reconsider d as Element of [:REAL,REAL:] by ZFMISC_1:def 2;
take d;
d is Element of [:REAL,REAL:] & g.i = ].d`1,d`2.] by A8;
hence thesis;
end;
ex f2 being FinSequence of [:REAL,REAL:] st len f2 = n & for i be Nat st
i in Seg n holds P[i,f2/.i] from FINSEQ_4:sch 1(A7);
then consider f2 being FinSequence of [:REAL,REAL:] such that
A9: len f2 = n and
A10: for i be Nat st i in Seg n holds
ex x be Element of [:REAL,REAL:] st f2/.i = x & g.i = ].x`1,x`2.];
reconsider f2 as n-element FinSequence of [:REAL,REAL:] by A9,CARD_1:def 7;
take f2;
thus x = y;
A11: for i be Nat st i in Seg n holds g.i = ].(f2/.i)`1,(f2/.i)`2.]
proof
let i be Nat;
assume i in Seg n;
then consider x be Element of [:REAL,REAL:] such that
A12: f2/.i = x and
A13: g.i = ].x`1,x`2.] by A10;
thus thesis by A12,A13;
end;
A14: for t be Element of REAL n st t in y
holds for i be Nat st i in Seg n holds t.i in ].(f2/.i)`1,(f2/.i)`2.]
proof
let t be Element of REAL n;
assume t in y;
then consider j0 be Function such that
A15: t = j0 and dom j0 = Seg n and
A16: for y be object st y in Seg n holds j0.y in g.y by A2,CARD_3:def 5,A4;
now
let i be Nat;
assume
A17: i in Seg n;
then t.i in g.i by A15,A16;
hence t.i in ].(f2/.i)`1,(f2/.i)`2.] by A17,A11;
end;
hence thesis;
end;
for t be Element of REAL n st
for i be Nat st i in Seg n holds t.i in ].(f2/.i)`1,(f2/.i)`2.]
holds t in y
proof
let t be Element of REAL n;
assume
A18: for i be Nat st i in Seg n holds t.i in ].(f2/.i)`1,(f2/.i)`2.];
reconsider j =t as Function;
t is Element of Funcs(Seg n,REAL) by FINSEQ_2:93; then
A19: ex j0 be Function st j = j0 & dom j0 = Seg n &
rng j0 c= REAL by FUNCT_2:def 2;
for y be object st y in Seg n holds j.y in g.y
proof
let y be object;
assume
A20: y in Seg n;
then reconsider y1=y as Nat;
g.y1 = ].(f2/.y1)`1,(f2/.y1)`2.] by A20,A11;
hence thesis by A20,A18;
end;
hence t in y by A19,A2,CARD_3:def 5,A4;
end;
hence thesis by A14;
end;
theorem Th32:
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 .])
proof
let x be object;
assume x in MeasurableRectangle(ProductLeftOpenIntervals(n));
then consider y being Subset of REAL n,
f being n-element FinSequence of [:REAL,REAL:]
such that
A1: x = y and
A2: (for t be Element of REAL n holds t in y iff
for i be Nat st i in Seg n holds t.i in ].(f/.i)`1,(f/.i)`2.]) by Th31;
consider x1 be Element of [:REAL n,REAL n:] such that
A3: for i being Nat st i in Seg n holds
(x1`1).i = (f/.i)`1 & (x1`2).i = (f/.i)`2 by Th13;
consider y1,z1 be object such that
A4: y1 in REAL n and
A5: z1 in REAL n and
A6: x1 = [y1,z1] by ZFMISC_1:def 2;
reconsider y1,z1 as Element of REAL n by A4,A5;
take y,y1,z1;
thus x = y by A1;
thus for s be object holds (s in y) iff (ex t be Element of REAL n st
s = t & for i be Nat st i in Seg n holds t.i in ]. y1.i, z1.i .])
proof
let s be object;
hereby
assume
A8: s in y;
then reconsider t = s as Element of REAL n;
now
take t;
thus s = t;
hereby
let i be Nat;
assume
A9: i in Seg n;
then (x1`1).i = (f/.i)`1 & (x1`2).i = (f/.i)`2 by A3;
hence t.i in ].y1.i,z1.i.] by A6,A8,A9,A2;
end;
end;
hence (ex t be Element of REAL n st s = t & for i be Nat st
i in Seg n holds t.i in ]. y1.i, z1.i .]);
end;
assume (ex t be Element of REAL n st s = t & for i be Nat st
i in Seg n holds t.i in ]. y1.i, z1.i .]);
then consider t be Element of REAL n such that
A10: s = t and
A11: for i be Nat st i in Seg n holds t.i in ]. y1.i, z1.i .];
now
let i be Nat;
assume
A12: i in Seg n;
then (x1`1).i = (f/.i)`1 & (x1`2).i = (f/.i)`2 by A3;
hence t.i in ].(f/.i)`1,(f/.i)`2.] by A11,A12,A6;
end;
hence s in y by A10,A2;
end;
end;
theorem
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
let x be set;
assume x in MeasurableRectangle(ProductLeftOpenIntervals(n));
then consider y being Subset of REAL n,
f being n-element FinSequence of [:REAL,REAL:] such that
A1: x = y and
A2: (for t be Element of REAL n holds t in y iff
for i be Nat st i in Seg n holds t.i in ].(f/.i)`1,(f/.i)`2.]) by Th31;
consider x1 be Element of [:REAL n,REAL n:] such that
A3: for i being Nat st i in Seg n holds
(x1`1).i = (f/.i)`1 & (x1`2).i = (f/.i)`2 by Th13;
consider y1,z1 be object such that
A4: y1 in REAL n and
A5: z1 in REAL n and
A6: x1 = [y1,z1] by ZFMISC_1:def 2;
reconsider y1,z1 as Element of REAL n by A4,A5;
take y1,z1;
for t be Element of REAL n holds t in x iff
for i be Nat st i in Seg n holds t.i in ]. y1.i, z1.i .]
proof
A7: now
let t be Element of REAL n;
assume
A8: t in x;
hereby
let i be Nat;
assume
A9: i in Seg n;
then (x1`1).i = (f/.i)`1 & (x1`2).i = (f/.i)`2 by A3;
hence t.i in ].y1.i,z1.i.] by A6,A8,A9,A1,A2;
end;
end;
now
let t be Element of REAL n;
assume
A10: for i be Nat st i in Seg n holds t.i in ]. y1.i, z1.i .];
now
let i be Nat;
assume
A11: i in Seg n;
then (x1`1).i = (f/.i)`1 & (x1`2).i = (f/.i)`2 by A3;
hence t.i in ].(f/.i)`1,(f/.i)`2.] by A10,A11,A6;
end;
hence t in x by A1,A2;
end;
hence thesis by A7;
end;
hence thesis;
end;
begin :: Finite Product of Right_Open_Intervals
definition
let n be non zero Nat;
func ProductRightOpenIntervals(n) -> ClassicalSemiringFamily of
ProductREAL(n) equals
Seg n --> the_set_of_all_right_open_real_bounded_intervals;
coherence
proof
reconsider S = Seg n --> the_set_of_all_right_open_real_bounded_intervals
as n-element FinSequence by Th6;
for i be Nat st i in Seg n holds S.i is with_empty_element
semi-diff-closed cap-closed Subset-Family of (ProductREAL(n)).i
proof
let i be Nat;
assume
A1: i in Seg n; then
A2: S.i = the_set_of_all_right_open_real_bounded_intervals &
(ProductREAL(n)).i = REAL by FUNCOP_1:7;
reconsider Si = S.i as Subset-Family of REAL by A1,FUNCOP_1:7;
thus thesis by A2,SRINGS_3:10;
end;
hence thesis by SRINGS_4:def 6;
end;
end;
reserve n for non zero Nat;
theorem
ProductRightOpenIntervals(n) = Seg n --> the set of all [.a,b.[ where
a,b is Real;
theorem Th33:
MeasurableRectangle(ProductRightOpenIntervals(n)) is Semiring of REAL n
proof
MeasurableRectangle(ProductRightOpenIntervals(n)) is Semiring of
product ProductREAL(n) by SRINGS_4:40;
hence thesis by Th7;
end;
theorem
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
let x be object;
assume
A1: x in MeasurableRectangle(ProductRightOpenIntervals(n));
MeasurableRectangle(ProductRightOpenIntervals(n)) is
Subset-Family of REAL n by Th33;
then reconsider y = x as Subset of REAL n by A1;
reconsider x0 = x as set by TARSKI:1;
consider g be Function such that
A2: x = product g and
A3: g in product ProductRightOpenIntervals(n) by A1,SRINGS_4:def 4;
dom ProductRightOpenIntervals(n) = Seg n by FUNCOP_1:13; then
A4: dom g = Seg n by A3,CARD_3:9;
take y;
thus x = y;
now
let i be Nat;
assume
A5: i in Seg n;
then i in dom ProductRightOpenIntervals(n) by FUNCOP_1:13;
then g.i in (ProductRightOpenIntervals(n)).i by A3,CARD_3:9;
then g.i in the set of all [.a,b.[ where a,b is Real by A5,FUNCOP_1:7;
then consider a,b be Real such that
A6: g.i = [.a,b.[;
hereby
take a,b;
now
let t be Element of REAL n;
assume t in y;
then consider j0 be Function such that
A7: t=j0 and
dom j0 = Seg n and
A8: for u be object st u in Seg n holds j0.u in g.u
by A2,CARD_3:def 5,A4;
thus t.i in [.a,b.[ by A7,A6,A8,A5;
end;
hence ex a,b being Real st
for t be Element of REAL n st t in y holds t.i in [.a,b.[;
end;
hence ex a,b being Real st
for t be Element of REAL n st t in y holds t.i in [.a,b.[;
end;
hence thesis;
end;
theorem Th34:
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.[)
proof
let x be object;
assume
A1: x in MeasurableRectangle(ProductRightOpenIntervals(n));
MeasurableRectangle(ProductRightOpenIntervals(n)) is
Subset-Family of REAL n by Th33;
then reconsider y = x as Subset of REAL n by A1;
take y;
reconsider x0 = x as set by TARSKI:1;
consider g be Function such that
A2: x = product g and
A3: g in product ProductRightOpenIntervals(n) by A1,SRINGS_4:def 4;
dom ProductRightOpenIntervals(n) = Seg n by FUNCOP_1:13; then
A4: dom g = Seg n by A3,CARD_3:9;
A5: now
let i be Nat;
assume
A6: i in Seg n;
then i in dom ProductRightOpenIntervals(n) by FUNCOP_1:13;
then g.i in (ProductRightOpenIntervals(n)).i by A3,CARD_3:9;
then g.i in the_set_of_all_right_open_real_bounded_intervals
by A6,FUNCOP_1:7;
hence ex a,b be Real st g.i = [.a,b.[;
end;
defpred P[Nat,set] means ex x be Element of [:REAL,REAL:] st $2 = x &
g.$1 = [.x`1,x`2.[;
A7: for i be Nat st i in Seg n holds ex d be Element of [:REAL,REAL:] st P[i,d]
proof
let i be Nat;
assume i in Seg n;
then consider a,b be Real such that
A8: g.i = [.a,b.[ by A5;
set d = [a,b];
a in REAL & b in REAL by XREAL_0:def 1;
then reconsider d as Element of [:REAL,REAL:] by ZFMISC_1:def 2;
take d;
d is Element of [:REAL,REAL:] & g.i = [.d`1,d`2.[ by A8;
hence thesis;
end;
ex f2 being FinSequence of [:REAL,REAL:] st len f2 = n & for i be Nat st
i in Seg n holds P[i,f2/.i] from FINSEQ_4:sch 1(A7);
then consider f2 being FinSequence of [:REAL,REAL:] such that
A9: len f2 = n and
A10: for i be Nat st i in Seg n holds
ex x be Element of [:REAL,REAL:] st f2/.i = x & g.i = [.x`1,x`2.[;
reconsider f2 as n-element FinSequence of [:REAL,REAL:] by A9,CARD_1:def 7;
take f2;
thus x = y;
A11: for i be Nat st i in Seg n holds g.i = [.(f2/.i)`1,(f2/.i)`2.[
proof
let i be Nat;
assume i in Seg n;
then consider x be Element of [:REAL,REAL:] such that
A12: f2/.i = x and
A13: g.i = [.x`1,x`2.[ by A10;
thus thesis by A12,A13;
end;
A14: for t be Element of REAL n st t in y
holds for i be Nat st i in Seg n holds t.i in [.(f2/.i)`1,(f2/.i)`2.[
proof
let t be Element of REAL n;
assume t in y;
then consider j0 be Function such that
A15: t = j0 and dom j0 = Seg n and
A16: for y be object st y in Seg n holds j0.y in g.y by A2,CARD_3:def 5,A4;
let i be Nat;
assume
A17: i in Seg n;
then t.i in g.i by A15,A16;
hence t.i in [.(f2/.i)`1,(f2/.i)`2.[ by A17,A11;
end;
for t be Element of REAL n st
for i be Nat st i in Seg n holds t.i in [.(f2/.i)`1,(f2/.i)`2.[
holds t in y
proof
let t be Element of REAL n;
assume
A18: for i be Nat st i in Seg n holds t.i in [.(f2/.i)`1,(f2/.i)`2.[;
reconsider j =t as Function;
t is Element of Funcs(Seg n,REAL) by FINSEQ_2:93; then
A19: ex j0 be Function st j = j0 & dom j0 = Seg n &
rng j0 c= REAL by FUNCT_2:def 2;
for y be object st y in Seg n holds j.y in g.y
proof
let y be object;
assume
A20: y in Seg n;
then reconsider y1=y as Nat;
g.y1 = [.(f2/.y1)`1,(f2/.y1)`2.[ by A20,A11;
hence thesis by A20,A18;
end;
hence t in y by A19,A2,CARD_3:def 5,A4;
end;
hence thesis by A14;
end;
theorem Th35:
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 .[)
proof
let x be object;
assume x in MeasurableRectangle(ProductRightOpenIntervals(n));
then consider y being Subset of REAL n,
f being n-element FinSequence of [:REAL,REAL:] such that
A1: x = y and
A2: (for t be Element of REAL n holds t in y iff
for i be Nat st i in Seg n holds t.i in [.(f/.i)`1,(f/.i)`2.[) by Th34;
consider x1 be Element of [:REAL n,REAL n:] such that
A3: for i being Nat st i in Seg n holds
(x1`1).i = (f/.i)`1 & (x1`2).i = (f/.i)`2 by Th13;
consider y1,z1 be object such that
A4: y1 in REAL n and
A5: z1 in REAL n and
A6: x1 = [y1,z1] by ZFMISC_1:def 2;
reconsider y1,z1 as Element of REAL n by A4,A5;
take y,y1,z1;
thus x = y by A1;
thus for s be object holds s in y iff (ex t be Element of REAL n st
s = t & for i be Nat st i in Seg n holds t.i in [. y1.i, z1.i .[)
proof
let s be object;
hereby
assume
A8: s in y;
then reconsider t = s as Element of REAL n;
now
take t;
thus s = t;
hereby
let i be Nat;
assume
A9: i in Seg n;
then (x1`1).i = (f/.i)`1 & (x1`2).i = (f/.i)`2 by A3;
hence t.i in [.y1.i,z1.i.[ by A6,A8,A9,A2;
end;
end;
hence (ex t be Element of REAL n st s = t & for i be Nat st
i in Seg n holds t.i in [. y1.i, z1.i .[);
end;
given t be Element of REAL n such that
A10: s = t and
A11: for i be Nat st i in Seg n holds t.i in [. y1.i, z1.i .[;
now
let i be Nat;
assume
A12: i in Seg n;
then (x1`1).i = (f/.i)`1 & (x1`2).i = (f/.i)`2 by A3;
hence t.i in [.(f/.i)`1,(f/.i)`2.[ by A11,A12,A6;
end;
hence s in y by A10,A2;
end;
end;
theorem
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
let x be set;
assume x in MeasurableRectangle(ProductRightOpenIntervals(n));
then consider y being Subset of REAL n,
f being n-element FinSequence of [:REAL,REAL:] such that
A1: x = y and
A2: (for t be Element of REAL n holds t in y iff
for i be Nat st i in Seg n holds t.i in [.(f/.i)`1,(f/.i)`2.[) by Th34;
consider x1 be Element of [:REAL n,REAL n:] such that
A3: for i being Nat st i in Seg n holds
(x1`1).i = (f/.i)`1 & (x1`2).i = (f/.i)`2 by Th13;
consider y1,z1 be object such that
A4: y1 in REAL n and
A5: z1 in REAL n and
A6: x1 = [y1,z1] by ZFMISC_1:def 2;
reconsider y1,z1 as Element of REAL n by A4,A5;
take y1,z1;
for t be Element of REAL n holds t in x iff
for i be Nat st i in Seg n holds t.i in [. y1.i, z1.i .[
proof
A7: now
let t be Element of REAL n;
assume
A8: t in x;
hereby
let i be Nat;
assume
A9: i in Seg n;
then (x1`1).i = (f/.i)`1 & (x1`2).i = (f/.i)`2 by A3;
hence t.i in [.y1.i,z1.i.[ by A6,A8,A9,A1,A2;
end;
end;
now
let t be Element of REAL n;
assume
A10: for i be Nat st i in Seg n holds t.i in [. y1.i, z1.i .[;
now
let i be Nat;
assume
A11: i in Seg n;
then (x1`1).i = (f/.i)`1 & (x1`2).i = (f/.i)`2 by A3;
hence t.i in [.(f/.i)`1,(f/.i)`2.[ by A10,A11,A6;
end;
hence t in x by A1,A2;
end;
hence thesis by A7;
end;
hence thesis;
end;
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 :Def2:
for f being object holds f in it iff
ex g being Function st f = product g & g in product (Seg n --> X);
existence
proof
defpred P[object] means
ex g be Function st $1 = product g & g in product (Seg n --> X);
consider Y be set such that
A1: for x being object holds
x in Y iff x in bool Funcs(dom (Seg n --> X), union Union (Seg n --> X))
& P[x] from XBOOLE_0:sch 1;
take Y;
now
thus for x be object st x in Y holds
ex g be Function st x = product g & g in product (Seg n --> X) by A1;
let x be object;
assume
A2: ex g be Function st x = product g & g in product (Seg n --> X);
given g be Function such that
A3: x = product g and
A4: g in product (Seg n --> X);
A5: dom g = dom (Seg n --> X) by A4,CARD_3:9;
rng g c= Union (Seg n --> X)
proof
let t be object;
assume t in rng g;
then consider u be object such that
A6: u in dom g and
A7: t=g.u by FUNCT_1:def 3;
consider h be Function such that
A8: g = h and
A9: dom h = dom (Seg n --> X) and
A10: for v be object st v in dom (Seg n --> X) holds
h.v in (Seg n --> X).v by A4,CARD_3:def 5;
t in (Seg n --> X).u & (Seg n --> X).u in rng (Seg n --> X)
by A8,A9,A10,A6,A7,FUNCT_1:def 3;
hence thesis by TARSKI:def 4;
end;
then Union g c= union Union (Seg n --> X) by ZFMISC_1:77;
then Funcs(dom g,Union g) c=
Funcs(dom (Seg n --> X), union Union (Seg n --> X))
by A5,FUNCT_5:56; then
A11: bool Funcs(dom g,Union g) c=
bool Funcs(dom (Seg n --> X), union Union (Seg n --> X))
by ZFMISC_1:67;
product g c= Funcs(dom g, Union g) by FUNCT_6:1;
hence x in Y by A2,A1,A3,A11;
end;
hence thesis;
end;
uniqueness
proof
let S1,S2 be set such that
A12:for f being object holds f in S1 iff
ex g being Function st f = product g & g in product (Seg n --> X) and
A13:for f being object holds f in S2 iff
ex g being Function st f = product g & g in product (Seg n --> X);
now
let x be object;
x in S1 iff
ex g being Function st x = product g & g in product (Seg n --> X) by A12;
hence x in S1 iff x in S2 by A13;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th36:
Product(n,X) c= bool Funcs(dom (Seg n --> X), union Union (Seg n --> X))
proof
let x be object;
assume x in Product(n,X);
then consider g be Function such that
A1: x = product g and
A2: g in product (Seg n --> X) by Def2;
A3: dom g = dom (Seg n --> X) by A2,CARD_3:9;
rng g c= Union (Seg n --> X)
proof
let t be object;
assume t in rng g;
then consider u be object such that
A4: u in dom g and
A5: t=g.u by FUNCT_1:def 3;
consider h be Function such that
A6: g = h and
A7: dom h = dom (Seg n --> X) and
A8: for v be object st v in dom (Seg n --> X) holds h.v in (Seg n --> X).v
by A2,CARD_3:def 5;
t in (Seg n --> X).u & (Seg n --> X).u in rng (Seg n --> X)
by A6,A7,A8,A4,A5,FUNCT_1:def 3;
hence thesis by TARSKI:def 4;
end;
then Union g c= union Union (Seg n --> X) by ZFMISC_1:77;
then Funcs(dom g,Union g) c=
Funcs(dom (Seg n --> X), union Union (Seg n --> X))
by A3,FUNCT_5:56; then
A9: bool Funcs(dom g,Union g) c=
bool Funcs(dom (Seg n --> X), union Union (Seg n --> X))
by ZFMISC_1:67;
product g c= Funcs(dom g, Union g) by FUNCT_6:1;
hence thesis by A1,A9;
end;
theorem Th37:
Product(n,S) is Subset-Family of product (Seg n --> X)
proof
reconsider SPS=Product(n,S) as Subset of
bool Funcs(dom (Seg n --> S),union Union (Seg n -->S)) by Th36;
SPS c= bool product (Seg n --> X)
proof
let x be object;
assume
A1: x in SPS;
reconsider x1=x as set by TARSKI:1;
x1 c= product (Seg n --> X)
proof
let t be object;
assume
A2: t in x1;
consider g be Function such that
A3: x1 = product g and
A4: g in product (Seg n --> S) by A1,Def2;
A5: dom g = dom (Seg n --> S) by A4,CARD_3:9;
consider u be Function such that
A7: t=u and
A8: dom u = dom g and
A9: for v be object st v in dom g holds u.v in g.v by A2,A3,CARD_3:def 5;
consider w be Function such that
A10: g=w and
dom w = dom (Seg n --> S) and
A12: for y be object st y in dom (Seg n --> S) holds
w.y in (Seg n --> S).y by A4,CARD_3:def 5;
A13: dom (Seg n --> S) = Seg n & dom (Seg n --> X) = Seg n by FUNCOP_1:13;
now
let a be object;
assume
A14: a in dom (Seg n --> X);
then reconsider a1=a as Nat;
u.a in g.a & g.a in (Seg n --> S).a by A14,A13,A10,A12,A9,A5;
then
A15: u.a in union ((Seg n --> S).a) & a in Seg n
by A14,TARSKI:def 4;
union ((Seg n --> S).a) c= (Seg n --> X).a
proof
A16: (Seg n --> S).a = S & (Seg n --> X).a = X by A14,FUNCOP_1:7;
union S c= union bool X by ZFMISC_1:77;
hence thesis by A16,ZFMISC_1:81;
end;
hence u.a in (Seg n --> X).a by A15;
end;
hence t in product (Seg n --> X) by A13,A5,A8,A7,CARD_3:def 5;
end;
hence x in bool product (Seg n --> X);
end;
hence thesis;
end;
theorem Th38:
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
proof
let S be non empty Subset-Family of X;
thus Product(n,S) c= the set of all product f where f is Tuple of n,S
proof
let x be object;
assume x in Product(n,S);
then consider g being Function such that
A1: x = product g and
A2: g in product (Seg n --> S) by Def2;
g in n-tuples_on S by A2,Th8;
then g is Tuple of n,S by FINSEQ_2:131;
hence x in the set of all product f where f is Tuple of n,S by A1;
end;
thus the set of all product f where f is Tuple of n,S c= Product(n,S)
proof
let x be object;
assume x in the set of all product f where f is Tuple of n,S;
then consider f be Tuple of n,S such that
A3: x = product f;
f in n-tuples_on S by FINSEQ_2:131;
then f in product(Seg n --> S) by Th8;
hence thesis by A3,Def2;
end;
end;
theorem Th39:
for n being non zero Nat holds
Product(n,X) c= bool Funcs(Seg n, union X)
proof
let n be non zero Nat;
let x be object;
assume x in Product(n,X);
then consider g be Function such that
A1: x = product g and
A2: g in product (Seg n --> X) by Def2;
A3: dom g = dom (Seg n --> X) by A2,CARD_3:9;
rng g c= Union (Seg n --> X)
proof
let t be object;
assume t in rng g;
then consider u be object such that
A4: u in dom g and
A5: t = g.u by FUNCT_1:def 3;
consider h be Function such that
A6: g = h and
A7: dom h = dom (Seg n --> X) and
A8: for v be object st v in dom (Seg n --> X) holds h.v in (Seg n --> X).v
by A2,CARD_3:def 5;
t in (Seg n --> X).u & (Seg n --> X).u in rng (Seg n --> X)
by A6,A7,A8,A4,A5,FUNCT_1:def 3;
hence thesis by TARSKI:def 4;
end;
then Union g c= union Union (Seg n --> X) by ZFMISC_1:77;
then Funcs(dom g,Union g) c=
Funcs(dom (Seg n --> X), union Union (Seg n --> X))
by A3,FUNCT_5:56;
then bool Funcs(dom g,Union g) c=
bool Funcs(dom (Seg n --> X), union Union (Seg n --> X))
by ZFMISC_1:67;
then bool Funcs(dom g,Union g) c=
bool Funcs(Seg n, union Union (Seg n --> X)) by FUNCOP_1:13; then
A11: bool Funcs(dom g,Union g) c=
bool Funcs(Seg n, union X) by CARD_3:7;
product g c= Funcs(dom g, Union g) by FUNCT_6:1;
hence thesis by A1,A11;
end;
theorem Th40:
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)
proof
let n be non zero Nat,X be non empty set,S be non empty Subset-Family of X;
assume
A1: S <> {{}};
A2: Product(n,S) c= bool Funcs(Seg n,union S) by Th39;
union S c= union bool X by ZFMISC_1:77; then
A3: union S is non empty Subset of X by A1,ZFMISC_1:81,SCMYCIEL:18;
n-tuples_on X = Funcs(Seg n,X) &
n-tuples_on union S = Funcs(Seg n,union S) by FINSEQ_2:93;
then bool Funcs(Seg n,union S) c= bool Funcs(Seg n,X)
by A3,Th5,ZFMISC_1:67;
hence thesis by A2;
end;
theorem
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)
proof
let n be non zero Nat,X be non empty set,S be non empty Subset-Family of X;
assume S <> {{}};
then union Product(n,S) c= union bool Funcs(Seg n,X) by ZFMISC_1:77,Th40;
hence thesis by ZFMISC_1:81;
end;
registration
let n be Nat, X be non empty set;
cluster Product(n,X) -> non empty;
coherence
proof
X is non empty;
then consider x0 be object such that
A1: x0 in X;
reconsider x0 as Element of X by A1;
A2: product(Seg n --> X) = n-tuples_on X by Th8;
set f = product (n |-> x0);
f in Product(n,X) by A2,Def2;
hence thesis;
end;
end;
Lm1:
for X being non empty set,
S being non empty Subset-Family of X,
x being Element of Product(n,S) holds
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
let X be non empty set,
S be non empty Subset-Family of X,
x be Element of Product(n,S);
consider g be Function such that
A1: x = product g and
A2: g in product (Seg n --> S) by Def2;
g in n-tuples_on S by A2,Th8;
then reconsider g as Tuple of n,S by FINSEQ_2:131;
take g;
for t be Element of Funcs(Seg n,X) holds
(for i be Nat st i in Seg n holds t.i in g.i) iff
t in x
proof
let t be Element of Funcs(Seg n,X);
hereby
assume
A3: for i be Nat st i in Seg n holds t.i in g.i;
t in Funcs(Seg n,X);
then t in n-tuples_on X by FINSEQ_2:93;
then dom t = Seg n by FINSEQ_1:89; then
A4: dom t = dom g by FINSEQ_2:124;
for i be object st i in dom g holds t.i in g.i
proof
let i be object;
assume i in dom g;
then i in Seg n by FINSEQ_2:124;
hence t.i in g.i by A3;
end;
hence t in x by A1,A4,CARD_3:def 5;
end;
assume
A5: t in x;
hereby
let i be Nat;
assume
A6: i in Seg n;
consider h be Function such that
A7: t = h and
dom h = dom g and
A8: for u be object st u in dom g holds h.u in g.u by A5,A1,CARD_3:def 5;
i in dom g by A6,FINSEQ_2:124;
hence t.i in g.i by A8,A7;
end;
end;
hence thesis;
end;
Lm2:
for X being non empty set,
S being non empty Subset-Family of X,
x being Subset of Funcs(Seg n,X),
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
let X be non empty set,
S be non empty Subset-Family of X,
x be Subset of Funcs(Seg n,X),
s be Tuple of n,S;
assume
A1: for t be Element of Funcs(Seg n,X) holds t in x iff
(for i be Nat st i in Seg n holds t.i in s.i);
x = product s
proof
for u being object holds u in x iff
ex g be Function st u = g & dom g = dom s &
for v being object st v in dom s holds g.v in s.v
proof
let u be object;
hereby
assume
A2: u in x; then
A3: u in Funcs(Seg n,X);
reconsider u1 = u as Function by A2;
now
u1 in n-tuples_on X by A3,FINSEQ_2:93;
then dom u1 = Seg n by FINSEQ_1:89;
hence dom u1 = dom s by FINSEQ_2:124;
hereby
let v be object;
assume v in dom s;
then v in Seg n by FINSEQ_2:124;
hence u1.v in s.v by A1,A2;
end;
end;
hence ex g be Function st u = g & dom g = dom s &
for v being object st v in dom s holds g.v in s.v;
end;
given g be Function such that
A5: u = g and
A6: dom g = dom s and
A7: for v be object st v in dom s holds g.v in s.v;
now
thus dom g = Seg n by A6,FINSEQ_2:124;
thus rng g c= X
proof
let t be object;
assume t in rng g;
then consider a be object such that
A8: a in dom g and
A9: t = g.a by FUNCT_1:def 3;
g.a in s.a & s.a in rng s & rng s c= S by A6,A8,A7,FUNCT_1:3;
then g.a in s.a & s.a in S & union S c= union bool X
by ZFMISC_1:77;
hence thesis by A9;
end;
end; then
A10: g is Element of Funcs(Seg n,X) by FUNCT_2:def 2;
for i be Nat st i in Seg n holds g.i in s.i
proof
let i be Nat;
assume i in Seg n;
then i in dom s by FINSEQ_2:124;
hence g.i in s.i by A7;
end;
hence u in x by A1,A5,A10;
end;
hence thesis by CARD_3:def 5;
end;
then x in the set of all product f where f is Tuple of n,S;
hence thesis by Th38;
end;
theorem
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)
by Lm1,Lm2;
begin :: the set of all closed real bounded intervals
definition
func the_set_of_all_closed_real_bounded_intervals ->
Subset-Family of REAL equals the set of all [.a,b.] where a,b is Real;
coherence
proof
the set of all [.a,b.] where a,b is Real c= bool REAL
proof
let x be object;
assume x in the set of all [.a,b.] where a,b is Real;
then ex a0,b0 be Real st x = [.a0,b0.];
hence thesis;
end;
hence thesis;
end;
end;
theorem
the_set_of_all_closed_real_bounded_intervals =
{I where I is Subset of REAL : I is closed_interval}
proof
A1: the_set_of_all_closed_real_bounded_intervals c=
{I where I is Subset of REAL : I is closed_interval}
proof
let x be object;
assume x in the_set_of_all_closed_real_bounded_intervals;
then consider a,b be Real such that
A2: x = [.a,b.];
reconsider x1 = x as Subset of REAL by A2;
x1 is closed_interval by A2,MEASURE5:def 3;
hence thesis;
end;
{I where I is Subset of REAL : I is closed_interval} c=
the_set_of_all_closed_real_bounded_intervals
proof
let x be object;
assume x in {I where I is Subset of REAL : I is closed_interval};
then consider I0 be Subset of REAL such that
A3: x = I0 and
A4: I0 is closed_interval;
consider a,b being Real such that
A5: I0 = [.a,b.] by A4,MEASURE5:def 3;
thus thesis by A3,A5;
end;
hence thesis by A1;
end;
registration
cluster the_set_of_all_closed_real_bounded_intervals -> non empty;
coherence
proof
[. 0 , 0 .] in the_set_of_all_closed_real_bounded_intervals;
hence thesis;
end;
end;
registration
cluster the_set_of_all_closed_real_bounded_intervals ->
cap-closed with_empty_element with_countable_Cover;
coherence
proof
thus the_set_of_all_closed_real_bounded_intervals is cap-closed
proof
now
let x,y be set;
assume that
A1: x in the_set_of_all_closed_real_bounded_intervals and
A2: y in the_set_of_all_closed_real_bounded_intervals;
consider a1,b1 be Real such that
A3: x = [.a1,b1.] by A1;
consider a2,b2 be Real such that
A4: y = [.a2,b2.] by A2;
[.a1,b1.] /\ [.a2,b2.] = [.max(a1,a2),min(b1,b2).] by XXREAL_1:140;
hence x /\ y in the_set_of_all_closed_real_bounded_intervals by A3,A4;
end;
hence thesis by FINSUB_1:def 2;
end;
[. 1 , 0 .] = {} by XXREAL_1:29;
then {} in the_set_of_all_closed_real_bounded_intervals;
hence the_set_of_all_closed_real_bounded_intervals is with_empty_element;
ex XX be countable Subset of the_set_of_all_closed_real_bounded_intervals
st XX is Cover of REAL
proof
defpred F[object,object] means
$1 is Element of NAT & $2 in
the_set_of_all_closed_real_bounded_intervals &
ex x be real number st x=$1 & $2=[.-x,x.];
A5: for x be object st x in NAT holds ex y be object st y in
the_set_of_all_closed_real_bounded_intervals & F[x,y]
proof
let x be object;
assume
A6: x in NAT;
then reconsider x as real number;
set y = [.-x,x.];
y in the_set_of_all_closed_real_bounded_intervals & F[x,y] by A6;
hence thesis;
end;
consider f be Function such that
A7: dom f=NAT & rng f c= the_set_of_all_closed_real_bounded_intervals and
A8: for x be object st x in NAT holds
F[x,f.x] from FUNCT_1:sch 6(A5);
A9: rng f is Subset-Family of REAL by A7,XBOOLE_1:1;
A10: rng f is countable
proof
reconsider f as SetSequence of REAL by A7,A9,RELSET_1:4,FUNCT_2:def 1;
rng f is countable by TOPGEN_4:58;
hence thesis;
end;
rng f is Cover of REAL
proof
Union f = REAL
proof
thus Union f c= REAL
proof
let x be object;
assume x in Union f;
then consider t be object such that
A11: t in dom f & x in f.t by CARD_5:2;
consider x0 be real number such that
A12: x0 = t & f.t = [.-x0,x0.] by A7,A8,A11;
thus thesis by A11,A12;
end;
for x be object st x in REAL holds x in Union f
proof
let x be object;
assume x in REAL;
then reconsider x as Real;
consider n be Element of NAT such that
A13: |.x.| <=n by MESFUNC1:8;
consider z be real number such that
A14: z = n & f.n = [.-z,z.] by A8;
-n <= x & x <= n by A13,ABSVALUE:5;
then x in f.n & f.n in rng f by A14,XXREAL_1:1,A7,FUNCT_1:def 3;
hence thesis by TARSKI:def 4;
end;
hence thesis;
end;
hence thesis by A9,SETFAM_1:45;
end;
hence thesis by A7,A10;
end;
hence the_set_of_all_closed_real_bounded_intervals is
with_countable_Cover by SRINGS_1:def 4;
end;
end;
theorem
for n being Nat holds Seg n -->
the_set_of_all_closed_real_bounded_intervals is n-element FinSequence
proof
let n be Nat;
reconsider f = Seg n --> the_set_of_all_closed_real_bounded_intervals as
FinSequence;
dom f is n-element by FUNCOP_1:13;
then card dom f = n by CARD_1:def 7;
then card f = n by CARD_1:62;
hence thesis by CARD_1:def 7;
end;
begin :: The set of all open real bounded intervals
definition
func the_set_of_all_open_real_bounded_intervals ->
Subset-Family of REAL equals the set of all ].a,b.[ where a,b is Real;
coherence
proof
the set of all ].a,b.[ where a,b is Real c= bool REAL
proof
let x be object;
assume x in the set of all ].a,b.[ where a,b is Real;
then ex a0,b0 be Real st x = ].a0,b0.[;
hence thesis;
end;
hence thesis;
end;
end;
theorem
the_set_of_all_open_real_bounded_intervals c=
{I where I is Subset of REAL : I is open_interval}
proof
let x be object;
assume x in the_set_of_all_open_real_bounded_intervals;
then consider a,b be Real such that
A2: x = ].a,b.[;
reconsider x1 = x as Subset of REAL by A2;
a is Element of ExtREAL & b is Element of ExtREAL
by NUMBERS:31,XREAL_0:def 1;
then x1 is open_interval by A2,MEASURE5:def 2;
hence thesis;
end;
registration
cluster the_set_of_all_open_real_bounded_intervals -> non empty;
coherence
proof
]. 0 , 0 .[ in the_set_of_all_open_real_bounded_intervals;
hence thesis;
end;
end;
registration
cluster the_set_of_all_open_real_bounded_intervals -> cap-closed
with_empty_element with_countable_Cover;
coherence
proof
thus the_set_of_all_open_real_bounded_intervals is cap-closed
proof
now
let x,y be set;
assume that
A1: x in the_set_of_all_open_real_bounded_intervals and
A2: y in the_set_of_all_open_real_bounded_intervals;
consider a1,b1 be Real such that
A3: x = ].a1,b1.[ by A1;
consider a2,b2 be Real such that
A4: y = ].a2,b2.[ by A2;
].a1,b1.[ /\ ].a2,b2.[ = ].max(a1,a2),min(b1,b2).[ by XXREAL_1:142;
hence x /\ y in the_set_of_all_open_real_bounded_intervals by A3,A4;
end;
hence thesis by FINSUB_1:def 2;
end;
]. 1 , 0 .[ = {} by XXREAL_1:28;
then {} in the_set_of_all_open_real_bounded_intervals;
hence the_set_of_all_open_real_bounded_intervals is with_empty_element;
ex XX be countable Subset of the_set_of_all_open_real_bounded_intervals
st XX is Cover of REAL
proof
defpred F[object,object] means
$1 is Element of NAT & $2 in the_set_of_all_open_real_bounded_intervals &
ex x be real number st x=$1 & $2=].-x,x.[;
A5: for x be object st x in NAT holds ex y be object st y in
the_set_of_all_open_real_bounded_intervals & F[x,y]
proof
let x be object;
assume
A6: x in NAT;
then reconsider x as real number;
set y = ].-x,x.[;
y in the_set_of_all_open_real_bounded_intervals & F[x,y] by A6;
hence thesis;
end;
consider f be Function such that
A7: dom f=NAT & rng f c= the_set_of_all_open_real_bounded_intervals and
A8: for x be object st x in NAT holds
F[x,f.x] from FUNCT_1:sch 6(A5);
A9: rng f is Subset-Family of REAL by A7,XBOOLE_1:1;
A10: rng f is countable
proof
reconsider f as SetSequence of REAL by A7,A9,RELSET_1:4,FUNCT_2:def 1;
rng f is countable by TOPGEN_4:58;
hence thesis;
end;
rng f is Cover of REAL
proof
Union f = REAL
proof
thus Union f c= REAL
proof
let x be object;
assume x in Union f;
then consider t be object such that
A11: t in dom f & x in f.t by CARD_5:2;
consider x0 be real number such that
A12: x0 = t & f.t = ].-x0,x0.[ by A7,A8,A11;
thus thesis by A11,A12;
end;
for x be object st x in REAL holds x in Union f
proof
let x be object;
assume x in REAL;
then reconsider x as Real;
consider n be Element of NAT such that
A13: |.x.| <=n by MESFUNC1:8;
consider z be real number such that
A14: z = n+1 & f.(n+1) = ].-z,z.[ by A8;
A15: -n <= x & x <= n by A13,ABSVALUE:5;
-n-1 < -n by XREAL_1:146;
then -(n+1) < x & x < (n+1) by A15,XXREAL_0:2,XREAL_1:145;
then x in f.(n+1) & f.(n+1) in rng f
by A14,A7,FUNCT_1:def 3,XXREAL_1:4;
hence thesis by TARSKI:def 4;
end;
hence thesis;
end;
hence thesis by A9,SETFAM_1:45;
end;
hence thesis by A7,A10;
end;
hence the_set_of_all_open_real_bounded_intervals is
with_countable_Cover by SRINGS_1:def 4;
end;
end;
theorem
for n being Nat holds Seg n --> the_set_of_all_open_real_bounded_intervals is
n-element FinSequence
proof
let n be Nat;
reconsider f = Seg n --> the_set_of_all_open_real_bounded_intervals as
FinSequence;
dom f is n-element by FUNCOP_1:13;
then card dom f = n by CARD_1:def 7;
then card f = n by CARD_1:62;
hence thesis by CARD_1:def 7;
end;
begin :: n-dimensional Subset-Family of REAL
reserve n for Nat,
S for Subset-Family of REAL;
theorem Th41:
Product(n,S) is Subset-Family of REAL n
proof
Product(n,S) is Subset-Family of product(Seg n --> REAL) by Th37;
hence thesis by Th7;
end;
definition
let n,S;
redefine func Product(n,S) -> Subset-Family of REAL n; :: redefines Product (SRINGS_5, definition)
coherence by Th41;
end;
theorem Th42:
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
proof
let S be non empty Subset-Family of REAL, x being Subset of REAL n;
A1: x is Subset of Funcs(Seg n,REAL) by FINSEQ_2:93;
thus x is Element of Product(n,S) implies (ex s be Tuple of n,S st
(for t be Element of REAL n holds (for i be Nat st i in Seg n holds
t.i in s.i) iff (t in x)))
proof
assume x is Element of Product(n,S);
then consider s be Tuple of n,S such that
A2: (for t be Element of Funcs(Seg n,REAL) holds (for i be Nat st
i in Seg n holds t.i in s.i) iff (t in x)) by Lm1;
take s;
for t be Element of REAL n holds (for i be Nat st i in Seg n holds
t.i in s.i) iff (t in x)
proof
let t be Element of REAL n;
t is Element of Funcs(Seg n,REAL) by FINSEQ_2:93;
hence thesis by A2;
end;
hence thesis;
end;
thus (ex s be Tuple of n,S st (for t be Element of REAL n holds
(for i be Nat st i in Seg n holds t.i in s.i) iff (t in x))) implies
x is Element of Product(n,S)
proof
given s be Tuple of n,S such that
A3: (for t be Element of REAL n holds (for i be Nat st i in Seg n holds
t.i in s.i) iff t in x);
ex s be Tuple of n,S st for t be Element of Funcs(Seg n,REAL) holds
(for i be Nat st i in Seg n holds t.i in s.i) iff (t in x)
proof
take s;
let t be Element of Funcs(Seg n,REAL);
t is Element of REAL n by FINSEQ_2:93;
hence (for i be Nat st i in Seg n holds t.i in s.i) iff (t in x) by A3;
end;
hence thesis by A1,Lm2;
end;
end;
theorem Th43:
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.]
proof
let n being non zero Nat,
s being Tuple of n,the_set_of_all_closed_real_bounded_intervals;
s in Funcs(Seg n,the_set_of_all_closed_real_bounded_intervals) by Th9;
then consider f be Function such that
A1: s = f and
A2: dom f = Seg n and
rng f c= the_set_of_all_closed_real_bounded_intervals by FUNCT_2:def 2;
defpred P[object,object] means ex f be Element of [:REAL,REAL:] st
f = $2 & s.$1=[.(f`1),(f`2).];
A3: for i be Nat st i in Seg n ex d be Element of [:REAL,REAL:] st P[i,d]
proof
let i be Nat;
assume i in Seg n;
then s.i in rng s by A1,A2,FUNCT_1:3;
then s.i in the set of all [.a,b.] where a,b is Real;
then consider a,b be Real such that
A4: s.i = [.a,b.];
a in REAL & b in REAL by XREAL_0:def 1;
then reconsider d = [a,b] as Element of [:REAL,REAL:]
by ZFMISC_1:def 2;
take d;
s.i = [.(d`1),(d`2).] by A4;
hence thesis;
end;
consider f being FinSequence of [:REAL,REAL:] such that
A5: len f = n and
A6: for i being Nat st i in Seg n holds P[i,f/.i] from FINSEQ_4:sch 1(A3);
reconsider f as n-element FinSequence of [:REAL,REAL:]
by A5,CARD_1:def 7;
consider z be Element of [:REAL n,REAL n:] such that
A7: for i being Nat st i in Seg n holds
(z`1).i = (f/.i)`1 & (z`2).i = (f/.i)`2 by Th13;
reconsider a = z`1,b = z`2 as Element of REAL n;
take a,b;
let i be Nat;
assume i in Seg n;
then a.i = (f/.i)`1 & b.i = (f/.i)`2 & P[i,f/.i] by A6,A7;
hence s.i = [.a.i,b.i.];
end;
theorem
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 .])))
proof
let n being non zero Nat,
x be Element of Product(n,the_set_of_all_closed_real_bounded_intervals);
consider s being Tuple of n,the_set_of_all_closed_real_bounded_intervals
such that
A1: 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 by Th42;
consider a,b being Element of REAL n such that
A2: for i being Nat st i in Seg n holds s.i = [.a.i,b.i.] by Th43;
take a,b;
let t be Element of REAL n;
hereby
assume
A3: t in x;
thus for i be Nat st i in Seg n holds t.i in [.a.i,b.i.]
proof
let i be Nat;
assume
A4: i in Seg n;
then s.i = [.a.i,b.i.] by A2;
hence t.i in [.a.i,b.i.] by A1,A3,A4;
end;
end;
assume
A5: for i be Nat st i in Seg n holds t.i in [.a.i,b.i.];
for i be Nat st i in Seg n holds t.i in s.i
proof
let i be Nat;
assume
A6: i in Seg n;
then s.i = [.a.i,b.i.] by A2;
hence t.i in s.i by A6,A5;
end;
hence t in x by A1;
end;
theorem
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)
proof
let n be non zero Nat, x be Subset of REAL n,
a,b be Element of REAL n;
assume
A1: for t be Element of REAL n holds
(t in x) iff
(for i be Nat st i in Seg n holds t.i in [.a.i,b.i.]);
defpred P[object,object] means ex n be Nat st
$1 = n & $2 = [.a.n,b.n.];
A2: for i be Nat st i in Seg n ex d be Element of
the_set_of_all_closed_real_bounded_intervals st P[i,d]
proof
let i be Nat;
assume i in Seg n;
set d = [.a.i,b.i.];
take d;
d in the set of all [.a,b.] where a,b is Real;
hence d is Element of the_set_of_all_closed_real_bounded_intervals;
thus P[i,d];
end;
ex g being FinSequence of the_set_of_all_closed_real_bounded_intervals st
len g = n & for i be Nat st i in Seg n holds P[i,g/.i]
from FINSEQ_4:sch 1(A2);
then consider g be FinSequence of
the_set_of_all_closed_real_bounded_intervals
such that
A3: len g = n and
A4: for i be Nat st i in Seg n holds P[i,g/.i];
A5: for i be Nat st i in Seg n holds g.i = [.a.i,b.i.]
proof
let i be Nat;
assume
A6: i in Seg n;
then P[i,g/.i] by A4;
then consider m be object such that
A7: m = i and
A8: g/.m = [.a.m,b.m.];
i in dom g by A6,A3,FINSEQ_1:def 3;
hence thesis by A7,A8,PARTFUN1:def 6;
end;
ex g be Function st x = product g &
g in product(Seg n --> the_set_of_all_closed_real_bounded_intervals)
proof
take g;
thus x = product g
proof
for t be object holds t in x iff
ex h be Function st t = h & dom h = dom g &
for u be object st u in dom g holds h.u in g.u
proof
let t be object;
hereby
assume
A9: t in x;
then reconsider t1 = t as Element of REAL n;
A10: dom t1 = Seg n by FINSEQ_1:89;
now
thus dom t1 = dom g by A10,A3,FINSEQ_1:def 3;
thus for u be object st u in dom g holds t1.u in g.u
proof
let u be object;
assume
u in dom g; then
A11: u in Seg n by A3,FINSEQ_1:def 3;
then t1.u in [.a.u,b.u.] by A9,A1;
hence t1.u in g.u by A11,A5;
end;
end;
hence ex h be Function st t = h & dom h = dom g &
for u be object st u in dom g holds h.u in g.u;
end;
hereby
given h be Function such that
A12: t = h and
A13: dom h = dom g and
A14: for u be object st u in dom g holds h.u in g.u;
A15: for i be Nat st i in Seg n holds h.i in [.a.i,b.i.]
proof
let i be Nat;
assume
A16: i in Seg n;
then i in dom g by A3,FINSEQ_1:def 3;
then h.i in g.i by A14;
hence h.i in [.a.i,b.i.] by A16,A5;
end;
dom h = dom (Seg n --> REAL) & for u be object st
u in dom (Seg n --> REAL) holds h.u in (Seg n --> REAL).u
proof
dom h = Seg n by A13,A3,FINSEQ_1:def 3;
hence dom h = dom (Seg n --> REAL) by FUNCOP_1:13;
hereby
let u be object;
assume
A17: u in dom (Seg n --> REAL); then
A18: u in Seg n;
h.u in [.a.u,b.u.] & [.a.u,b.u.] c= REAL by A17,A15;
then h.u in REAL & u in dom g by A18,A3,FINSEQ_1:def 3;
hence h.u in (Seg n--> REAL).u by FUNCOP_1:7,A17;end;
end;
then h in product(Seg n --> REAL) by CARD_3:9;
then reconsider h as Element of REAL n by Th7;
h in x by A15,A1;
hence t in x by A12;
end;
end;
hence thesis by CARD_3:def 5;
end;
thus g in product(Seg n --> the_set_of_all_closed_real_bounded_intervals)
proof
A19: dom g = Seg n & dom (Seg n -->
the_set_of_all_closed_real_bounded_intervals) = Seg n
by A3,FINSEQ_1:def 3,FUNCOP_1:13;
for x be object st x in dom (Seg n -->
the_set_of_all_closed_real_bounded_intervals)
holds g.x in (Seg n --> the_set_of_all_closed_real_bounded_intervals).x
proof
let x be object;
assume
A20: x in dom (Seg n --> the_set_of_all_closed_real_bounded_intervals);
then g.x = [.a.x,b.x.] by A5;
then g.x in the_set_of_all_closed_real_bounded_intervals &
(Seg n --> the_set_of_all_closed_real_bounded_intervals).x =
the_set_of_all_closed_real_bounded_intervals by A20,FUNCOP_1:7;
hence thesis;
end;
hence thesis by A19,CARD_3:9;
end;
end;
hence thesis by Def2;
end;
theorem Th44:
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)
proof
let n be non zero Nat, x be Subset of REAL n,
a,b be Element of REAL n;
assume
A1: for t be Element of REAL n holds
t in x iff
(for i be Nat st i in Seg n holds t.i in ].a.i,b.i.]);
defpred P[object,object] means ex n be Nat st
$1 = n & $2 = ].a.n,b.n.];
A2: for i be Nat st i in Seg n ex d be Element of
the_set_of_all_left_open_real_bounded_intervals st P[i,d]
proof
let i be Nat;
assume i in Seg n;
set d = ].a.i,b.i.];
take d;
d in the set of all ].a,b.] where a,b is Real;
hence d is Element of the_set_of_all_left_open_real_bounded_intervals;
thus P[i,d];
end;
ex g being FinSequence of the_set_of_all_left_open_real_bounded_intervals
st len g = n & for i be Nat st i in Seg n holds P[i,g/.i]
from FINSEQ_4:sch 1(A2);
then consider g be FinSequence of
the_set_of_all_left_open_real_bounded_intervals
such that
A3: len g = n and
A4: for i be Nat st i in Seg n holds P[i,g/.i];
A5: for i be Nat st i in Seg n holds g.i = ].a.i,b.i.]
proof
let i be Nat;
assume
A6: i in Seg n;
then P[i,g/.i] by A4;
then consider m be object such that
A7: m = i and
A8: g/.m = ].a.m,b.m.];
i in dom g by A6,A3,FINSEQ_1:def 3;
hence thesis by A7,A8,PARTFUN1:def 6;
end;
ex g be Function st x = product g &
g in product(Seg n --> the_set_of_all_left_open_real_bounded_intervals)
proof
take g;
thus x = product g
proof
for t be object holds t in x iff
ex h be Function st t = h & dom h = dom g &
for u be object st u in dom g holds h.u in g.u
proof
let t be object;
hereby
assume
A9: t in x;
then reconsider t1 = t as Element of REAL n;
A10: dom t1 = Seg n by FINSEQ_1:89;
now
thus dom t1 = dom g by A10,A3,FINSEQ_1:def 3;
thus for u be object st u in dom g holds t1.u in g.u
proof
let u be object;
assume
u in dom g; then
A11: u in Seg n by A3,FINSEQ_1:def 3;
then t1.u in ].a.u,b.u.] by A9,A1;
hence t1.u in g.u by A11,A5;
end;
end;
hence ex h be Function st t = h & dom h = dom g &
for u be object st u in dom g holds h.u in g.u;
end;
hereby
given h be Function such that
A12: t = h and
A13: dom h = dom g and
A14: for u be object st u in dom g holds h.u in g.u;
A15: for i be Nat st i in Seg n holds h.i in ].a.i,b.i.]
proof
let i be Nat;
assume
A16: i in Seg n;
then i in dom g by A3,FINSEQ_1:def 3;
then h.i in g.i by A14;
hence h.i in ].a.i,b.i.] by A16,A5;
end;
dom h = dom (Seg n --> REAL) & for u be object st
u in dom (Seg n --> REAL) holds h.u in (Seg n --> REAL).u
proof
dom h = Seg n by A13,A3,FINSEQ_1:def 3;
hence dom h = dom (Seg n --> REAL) by FUNCOP_1:13;
hereby
let u be object;
assume
A17: u in dom (Seg n --> REAL); then
A18: u in Seg n;
h.u in ].a.u,b.u.] & ].a.u,b.u.] c= REAL by A17,A15;
then h.u in REAL & u in dom g by A18,A3,FINSEQ_1:def 3;
hence h.u in (Seg n--> REAL).u by FUNCOP_1:7,A17;end;
end;
then h in product(Seg n --> REAL) by CARD_3:9;
then reconsider h as Element of REAL n by Th7;
h in x by A15,A1;
hence t in x by A12;
end;
end;
hence thesis by CARD_3:def 5;
end;
thus g in product(Seg n -->
the_set_of_all_left_open_real_bounded_intervals)
proof
A19: dom g = Seg n & dom (Seg n -->
the_set_of_all_left_open_real_bounded_intervals) = Seg n
by A3,FINSEQ_1:def 3,FUNCOP_1:13;
for x be object st x in dom (Seg n -->
the_set_of_all_left_open_real_bounded_intervals)
holds g.x in (Seg n -->
the_set_of_all_left_open_real_bounded_intervals).x
proof
let x be object;
assume
A20: x in dom (Seg n --> the_set_of_all_left_open_real_bounded_intervals);
then g.x = ].a.x,b.x.] by A5;
then g.x in the_set_of_all_left_open_real_bounded_intervals &
(Seg n --> the_set_of_all_left_open_real_bounded_intervals).x =
the_set_of_all_left_open_real_bounded_intervals by A20,FUNCOP_1:7;
hence thesis;
end;
hence thesis by A19,CARD_3:9;
end;
end;
hence thesis by Def2;
end;
theorem Th45:
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)
proof
let n be non zero Nat, x be Subset of REAL n,
a,b be Element of REAL n;
assume
A1: for t be Element of REAL n holds
t in x iff
(for i be Nat st i in Seg n holds t.i in [.a.i,b.i.[);
defpred P[object,object] means ex n be Nat st
$1 = n & $2 = [.a.n,b.n.[;
A2: for i be Nat st i in Seg n ex d be Element of
the_set_of_all_right_open_real_bounded_intervals st P[i,d]
proof
let i be Nat;
assume i in Seg n;
set d = [.a.i,b.i.[;
take d;
d in the set of all [.a,b.[ where a,b is Real;
hence d is Element of the_set_of_all_right_open_real_bounded_intervals;
thus P[i,d];
end;
ex g being FinSequence of
the_set_of_all_right_open_real_bounded_intervals st len g = n &
for i be Nat st i in Seg n holds P[i,g/.i]
from FINSEQ_4:sch 1(A2);
then consider g be FinSequence of
the_set_of_all_right_open_real_bounded_intervals such that
A3: len g = n and
A4: for i be Nat st i in Seg n holds P[i,g/.i];
A5: for i be Nat st i in Seg n holds g.i = [.a.i,b.i.[
proof
let i be Nat;
assume
A6: i in Seg n;
then P[i,g/.i] by A4;
then consider m be object such that
A7: m = i and
A8: g/.m = [.a.m,b.m.[;
i in dom g by A6,A3,FINSEQ_1:def 3;
hence thesis by A7,A8,PARTFUN1:def 6;
end;
ex g be Function st x = product g &
g in product(Seg n --> the_set_of_all_right_open_real_bounded_intervals)
proof
take g;
thus x = product g
proof
for t be object holds t in x iff
ex h be Function st t = h & dom h = dom g &
for u be object st u in dom g holds h.u in g.u
proof
let t be object;
hereby
assume
A9: t in x;
then reconsider t1 = t as Element of REAL n;
A10: dom t1 = Seg n by FINSEQ_1:89;
now
thus dom t1 = dom g by A10,A3,FINSEQ_1:def 3;
thus for u be object st u in dom g holds t1.u in g.u
proof
let u be object;
assume
u in dom g; then
A11: u in Seg n by A3,FINSEQ_1:def 3;
then t1.u in [.a.u,b.u.[ by A9,A1;
hence t1.u in g.u by A11,A5;
end;
end;
hence ex h be Function st t = h & dom h = dom g &
for u be object st u in dom g holds h.u in g.u;
end;
hereby
given h be Function such that
A12: t = h and
A13: dom h = dom g and
A14: for u be object st u in dom g holds h.u in g.u;
A15: for i be Nat st i in Seg n holds h.i in [.a.i,b.i.[
proof
let i be Nat;
assume
A16: i in Seg n;
then i in dom g by A3,FINSEQ_1:def 3;
then h.i in g.i by A14;
hence h.i in [.a.i,b.i.[ by A16,A5;
end;
dom h = dom (Seg n --> REAL) & for u be object st
u in dom (Seg n --> REAL) holds h.u in (Seg n --> REAL).u
proof
dom h = Seg n by A13,A3,FINSEQ_1:def 3;
hence dom h = dom (Seg n --> REAL) by FUNCOP_1:13;
hereby
let u be object;
assume
A17: u in dom (Seg n --> REAL); then
A18: u in Seg n;
h.u in [.a.u,b.u.[ & [.a.u,b.u.[ c= REAL by A17,A15;
then h.u in REAL & u in dom g by A18,A3,FINSEQ_1:def 3;
hence h.u in (Seg n--> REAL).u by FUNCOP_1:7,A17;end;
end;
then h in product(Seg n --> REAL) by CARD_3:9;
then reconsider h as Element of REAL n by Th7;
h in x by A15,A1;
hence t in x by A12;
end;
end;
hence thesis by CARD_3:def 5;
end;
thus g in product(Seg n -->
the_set_of_all_right_open_real_bounded_intervals)
proof
A19: dom g = Seg n & dom (Seg n -->
the_set_of_all_right_open_real_bounded_intervals) = Seg n
by A3,FINSEQ_1:def 3,FUNCOP_1:13;
for x be object st x in dom (Seg n -->
the_set_of_all_right_open_real_bounded_intervals)
holds g.x in (Seg n -->
the_set_of_all_right_open_real_bounded_intervals).x
proof
let x be object;
assume
A20: x in dom (Seg n -->
the_set_of_all_right_open_real_bounded_intervals);
then g.x = [.a.x,b.x.[ by A5;
then g.x in the_set_of_all_right_open_real_bounded_intervals &
(Seg n --> the_set_of_all_right_open_real_bounded_intervals).x =
the_set_of_all_right_open_real_bounded_intervals by A20,FUNCOP_1:7;
hence thesis;
end;
hence thesis by A19,CARD_3:9;
end;
end;
hence thesis by Def2;
end;
theorem Th46:
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.]
proof
let n be non zero Nat,
s be Tuple of n,the_set_of_all_left_open_real_bounded_intervals;
s in Funcs(Seg n,the_set_of_all_left_open_real_bounded_intervals) by Th9;
then consider f be Function such that
A1: s = f and
A2: dom f = Seg n and
rng f c= the_set_of_all_left_open_real_bounded_intervals by FUNCT_2:def 2;
defpred P[object,object] means ex f be Element of [:REAL,REAL:] st
f = $2 & s.$1=].(f`1),(f`2).];
A3: for i be Nat st i in Seg n ex d be Element of [:REAL,REAL:] st P[i,d]
proof
let i be Nat;
assume i in Seg n;
then s.i in rng s by A1,A2,FUNCT_1:3;
then s.i in the set of all ].a,b.] where a,b is Real;
then consider a,b be Real such that
A4: s.i = ].a,b.];
a in REAL & b in REAL by XREAL_0:def 1;
then reconsider d = [a,b] as Element of [:REAL,REAL:]
by ZFMISC_1:def 2;
take d;
s.i = ].(d`1),(d`2).] by A4;
hence thesis;
end;
consider f being FinSequence of [:REAL,REAL:] such that
A5: len f = n and
A6: for i being Nat st i in Seg n holds P[i,f/.i] from FINSEQ_4:sch 1(A3);
reconsider f as n-element FinSequence of [:REAL,REAL:]
by A5,CARD_1:def 7;
consider z be Element of [:REAL n,REAL n:] such that
A7: for i being Nat st i in Seg n holds
(z`1).i = (f/.i)`1 & (z`2).i = (f/.i)`2 by Th13;
reconsider a = z`1,b = z`2 as Element of REAL n;
take a,b;
let i be Nat;
assume i in Seg n;
then a.i = (f/.i)`1 & b.i = (f/.i)`2 & P[i,f/.i] by A6,A7;
hence s.i = ].a.i,b.i.];
end;
theorem
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 .])))
proof
let n being non zero Nat,
x be Element of
Product(n,the_set_of_all_left_open_real_bounded_intervals);
consider s being Tuple of n,the_set_of_all_left_open_real_bounded_intervals
such that
A1: 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 by Th42;
consider a,b being Element of REAL n such that
A2: for i being Nat st i in Seg n holds s.i = ].a.i,b.i.] by Th46;
take a,b;
for t being Element of REAL n holds t in x iff (for i be Nat st i in Seg n
holds t.i in ].a.i,b.i.])
proof
let t be Element of REAL n;
hereby
assume
A3: t in x;
thus (for i be Nat st i in Seg n holds t.i in ].a.i,b.i.])
proof
let i be Nat;
assume
A4: i in Seg n;
then s.i = ].a.i,b.i.] by A2;
hence t.i in ].a.i,b.i.] by A1,A3,A4;
end;
end;
assume
A5: for i be Nat st i in Seg n holds t.i in ].a.i,b.i.];
for i be Nat st i in Seg n holds t.i in s.i
proof
let i be Nat;
assume
A6: i in Seg n;
then s.i = ].a.i,b.i.] by A2;
hence t.i in s.i by A6,A5;
end;
hence t in x by A1;
end;
hence thesis;
end;
theorem Th47:
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.[
proof
let n being non zero Nat,
s be Tuple of n,the_set_of_all_right_open_real_bounded_intervals;
s in Funcs(Seg n,the_set_of_all_right_open_real_bounded_intervals) by Th9;
then consider f be Function such that
A1: s = f and
A2: dom f = Seg n and
rng f c= the_set_of_all_right_open_real_bounded_intervals by FUNCT_2:def 2;
defpred P[object,object] means ex f be Element of [:REAL,REAL:] st
f = $2 & s.$1 = [.(f`1),(f`2).[;
A3: for i be Nat st i in Seg n ex d be Element of [:REAL,REAL:] st P[i,d]
proof
let i be Nat;
assume i in Seg n;
then s.i in rng s by A1,A2,FUNCT_1:3;
then s.i in the set of all [.a,b.[ where a,b is Real;
then consider a,b be Real such that
A4: s.i = [.a,b.[;
a in REAL & b in REAL by XREAL_0:def 1;
then reconsider d = [a,b] as Element of [:REAL,REAL:]
by ZFMISC_1:def 2;
take d;
s.i = [.(d`1),(d`2).[ by A4;
hence thesis;
end;
consider f being FinSequence of [:REAL,REAL:] such that
A5: len f = n and
A6: for i being Nat st i in Seg n holds P[i,f/.i] from FINSEQ_4:sch 1(A3);
reconsider f as n-element FinSequence of [:REAL,REAL:]
by A5,CARD_1:def 7;
consider z be Element of [:REAL n,REAL n:] such that
A7: for i being Nat st i in Seg n holds
(z`1).i = (f/.i)`1 & (z`2).i = (f/.i)`2 by Th13;
reconsider a = z`1,b = z`2 as Element of REAL n;
take a,b;
thus for i being Nat st i in Seg n holds s.i = [. a.i,b.i .[
proof
let i be Nat;
assume i in Seg n;
then a.i = (f/.i)`1 & b.i = (f/.i)`2 & P[i,f/.i] by A6,A7;
hence s.i = [.a.i,b.i.[;
end;
end;
theorem
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 .[)))
proof
let n being non zero Nat,
x be Element of
Product(n,the_set_of_all_right_open_real_bounded_intervals);
consider s being Tuple of n,
the_set_of_all_right_open_real_bounded_intervals such that
A1: 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 by Th42;
consider a,b being Element of REAL n such that
A2: for i being Nat st i in Seg n holds s.i = [.a.i,b.i.[ by Th47;
take a,b;
for t being Element of REAL n holds t in x iff (for i be Nat st i in Seg n
holds t.i in [.a.i,b.i.[)
proof
let t be Element of REAL n;
hereby
assume
A3: t in x;
thus for i be Nat st i in Seg n holds t.i in [.a.i,b.i.[
proof
let i be Nat;
assume
A4: i in Seg n;
then s.i = [.a.i,b.i.[ by A2;
hence t.i in [.a.i,b.i.[ by A1,A3,A4;
end;
end;
assume
A5: (for i be Nat st i in Seg n holds t.i in [.a.i,b.i.[);
for i be Nat st i in Seg n holds t.i in s.i
proof
let i be Nat;
assume
A6: i in Seg n;
then s.i = [.a.i,b.i.[ by A2;
hence t.i in s.i by A6,A5;
end;
hence t in x by A1;
end;
hence thesis;
end;
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
:Def3:
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
proof
defpred P[object,object] means ex S be Subset of REAL st
S = $2 & S = [.a.$1,b.$1.];
A1: for i be Nat st i in Seg n ex d being Element of bool REAL st P[i,d];
consider f being FinSequence of bool REAL such that
A2: len f = n and
A3: for i be Nat st i in Seg n holds P[i,f/.i] from FINSEQ_4:sch 1(A1);
A4: dom f = Seg n by A2,FINSEQ_1:def 3;
set s = product f;
s c= product(Seg n --> REAL)
proof
let t be object;
assume
A5: t in s;
then reconsider t1 = t as Function;
A6: dom t1 = dom f & for y be object st y in dom f holds t1.y in f.y
by A5,CARD_3:9;
now
dom (Seg n --> REAL) = Seg n by FUNCOP_1:13;
hence dom t1 = dom (Seg n --> REAL) by A6,A2,FINSEQ_1:def 3;
thus for y be object st y in dom (Seg n --> REAL) holds
t1.y in (Seg n --> REAL).y
proof
let y be object;
assume
A7: y in dom(Seg n-->REAL);
then y in Seg n;
then y in dom f by A2,FINSEQ_1:def 3;
then t1.y in f.y & f.y in bool REAL by A5,CARD_3:9,FINSEQ_2:11;
then t1.y in REAL;
hence thesis by A7,FUNCOP_1:7;
end;
end;
hence t in product(Seg n --> REAL) by CARD_3:9;
end;
then reconsider s as Subset of REAL n by Th7;
for x being object holds x in s iff ex y be Element of REAL n st
x = y & (for i be Nat st i in Seg n holds y.i in [.a.i,b.i.])
proof
let x be object;
thus x in s iff ex y be Element of REAL n st x = y &
(for i be Nat st i in Seg n holds y.i in [.a.i,b.i.])
proof
hereby
assume
A8: x in s;
then reconsider y = x as Element of REAL n;
take y;
thus x = y;
thus for i be Nat st i in Seg n holds y.i in [.a.i,b.i.]
proof
let i be Nat;
assume
A9: i in Seg n; then
A10: i in dom f by A2,FINSEQ_1:def 3; then
A11: y.i in f.i by A8,CARD_3:9;
consider S2 be Subset of REAL such that
A12: f/.i = S2 and
A13: S2 = [.a.i,b.i.] by A9,A3;
thus y.i in [.a.i,b.i.] by A10,A11,A12,A13,PARTFUN1:def 6;
end;
end;
given y be Element of REAL n such that
A14: x = y and
A15: for i be Nat st i in Seg n holds y.i in [.a.i,b.i.];
now
thus dom y = dom f by A4,FINSEQ_1:89;
thus for z being object st z in dom f holds y.z in f.z
proof
let z be object;
assume
A16: z in dom f; then
A17: z in Seg n by A2,FINSEQ_1:def 3;
then consider S2 be Subset of REAL such that
A18: f/.z = S2 and
A19: S2 = [.a.z,b.z.] by A3;
f/.z = f.z by A16,PARTFUN1:def 6;
hence y.z in f.z by A18,A19,A15,A17;
end;
end;
hence x in s by A14,CARD_3:9;
end;
end;
hence thesis;
end;
uniqueness
proof
let I1,I2 be Subset of REAL n such that
A20: for x being object holds x in I1 iff ex y being Element of REAL n st
x = y &
(for i be Nat st i in Seg n holds y.i in [.a.i,b.i.]) and
A21: for x being object holds x in I2 iff ex y being Element of REAL n st
x = y &
(for i be Nat st i in Seg n holds y.i in [.a.i,b.i.]);
thus I1 c= I2
proof
let x be object;
assume x in I1;
then consider y be Element of REAL n such that
A22: x = y and
A23: for i be Nat st i in Seg n holds y.i in [.a.i,b.i.] by A20;
thus x in I2 by A21,A23,A22;
end;
let x be object;
assume x in I2;
then consider y be Element of REAL n such that
A24:x = y and
A25:for i be Nat st i in Seg n holds y.i in [.a.i,b.i.] by A21;
thus x in I1 by A24,A25,A20;
end;
end;
definition
let n,a,b;
func OpenHyperInterval(a,b) -> Subset of REAL n means
:Def4:
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
proof
defpred P[object,object] means ex S be Subset of REAL st
S = $2 & S = ].a.$1,b.$1.[;
A1: for i be Nat st i in Seg n ex d being Element of bool REAL st P[i,d];
consider f being FinSequence of bool REAL such that
A2: len f = n and
A3: for i be Nat st i in Seg n holds P[i,f/.i] from FINSEQ_4:sch 1(A1);
A4: dom f = Seg n by A2,FINSEQ_1:def 3;
set s = product f;
s c= product(Seg n --> REAL)
proof
let t be object;
assume
A5: t in s;
then reconsider t1 = t as Function;
A6: dom t1 = dom f & for y be object st y in dom f holds t1.y in f.y
by A5,CARD_3:9;
now
dom (Seg n --> REAL) = Seg n by FUNCOP_1:13;
hence dom t1 = dom (Seg n --> REAL) by A6,A2,FINSEQ_1:def 3;
thus for y be object st y in dom (Seg n --> REAL) holds
t1.y in (Seg n --> REAL).y
proof
let y be object;
assume
A7: y in dom(Seg n-->REAL);
then y in Seg n;
then y in dom f by A2,FINSEQ_1:def 3;
then t1.y in f.y & f.y in bool REAL by A5,CARD_3:9,FINSEQ_2:11;
then t1.y in REAL;
hence thesis by A7,FUNCOP_1:7;
end;
end;
hence t in product(Seg n --> REAL) by CARD_3:9;
end;
then reconsider s as Subset of REAL n by Th7;
for x being object holds x in s iff ex y be Element of REAL n st
x = y & (for i be Nat st i in Seg n holds y.i in ].a.i,b.i.[)
proof
let x be object;
thus x in s iff ex y be Element of REAL n st x = y &
(for i be Nat st i in Seg n holds y.i in ].a.i,b.i.[)
proof
hereby
assume
A8: x in s;
then reconsider y = x as Element of REAL n;
take y;
thus x = y;
thus for i be Nat st i in Seg n holds y.i in ].a.i,b.i.[
proof
let i be Nat;
assume
A9: i in Seg n; then
A10: i in dom f by A2,FINSEQ_1:def 3; then
A11: y.i in f.i by A8,CARD_3:9;
consider S2 be Subset of REAL such that
A12: f/.i = S2 and
A13: S2 = ].a.i,b.i.[ by A9,A3;
thus y.i in ].a.i,b.i.[ by A10,A11,A12,A13,PARTFUN1:def 6;
end;
end;
given y be Element of REAL n such that
A14: x = y and
A15: for i be Nat st i in Seg n holds y.i in ].a.i,b.i.[;
now
thus dom y = dom f by A4,FINSEQ_1:89;
thus for z being object st z in dom f holds y.z in f.z
proof
let z be object;
assume
A16: z in dom f; then
A17: z in Seg n by A2,FINSEQ_1:def 3;
then consider S2 be Subset of REAL such that
A18: f/.z = S2 and
A19: S2 = ].a.z,b.z.[ by A3;
f/.z = f.z by A16,PARTFUN1:def 6;
hence y.z in f.z by A18,A19,A15,A17;
end;
end;
hence x in s by A14,CARD_3:9;
end;
end;
hence thesis;
end;
uniqueness
proof
let I1,I2 be Subset of REAL n such that
A20: for x being object holds x in I1 iff ex y being Element of REAL n st
x = y &
(for i be Nat st i in Seg n holds y.i in ].a.i,b.i.[) and
A21: for x being object holds x in I2 iff ex y being Element of REAL n st
x = y &
(for i be Nat st i in Seg n holds y.i in ].a.i,b.i.[);
thus I1 c= I2
proof
let x be object;
assume x in I1;
then consider y be Element of REAL n such that
A22: x = y and
A23: for i be Nat st i in Seg n holds y.i in ].a.i,b.i.[ by A20;
thus x in I2 by A21,A23,A22;
end;
let x be object;
assume x in I2;
then consider y be Element of REAL n such that
A24: x = y and
A25: for i be Nat st i in Seg n holds y.i in ].a.i,b.i.[ by A21;
thus x in I1 by A24,A25,A20;
end;
end;
definition
let n,a,b;
func LeftOpenHyperInterval(a,b) -> Subset of REAL n means
:Def5:
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
proof
defpred P[object,object] means ex S be Subset of REAL st
S = $2 & S = ].a.$1,b.$1.];
A1: for i be Nat st i in Seg n ex d being Element of bool REAL st P[i,d];
consider f being FinSequence of bool REAL such that
A2: len f = n and
A3: for i be Nat st i in Seg n holds P[i,f/.i] from FINSEQ_4:sch 1(A1);
A4: dom f = Seg n by A2,FINSEQ_1:def 3;
set s = product f;
s c= product(Seg n --> REAL)
proof
let t be object;
assume
A5: t in s;
then reconsider t1 = t as Function;
A6: dom t1 = dom f & for y be object st y in dom f holds t1.y in f.y
by A5,CARD_3:9;
now
dom (Seg n --> REAL) = Seg n by FUNCOP_1:13;
hence dom t1 = dom (Seg n --> REAL) by A6,A2,FINSEQ_1:def 3;
thus for y be object st y in dom (Seg n --> REAL) holds
t1.y in (Seg n --> REAL).y
proof
let y be object;
assume
A7: y in dom(Seg n-->REAL);
then y in Seg n;
then y in dom f by A2,FINSEQ_1:def 3;
then t1.y in f.y & f.y in bool REAL by A5,CARD_3:9,FINSEQ_2:11;
then t1.y in REAL;
hence thesis by A7,FUNCOP_1:7;
end;
end;
hence t in product(Seg n --> REAL) by CARD_3:9;
end;
then reconsider s as Subset of REAL n by Th7;
for x being object holds x in s iff ex y be Element of REAL n st
x = y & (for i be Nat st i in Seg n holds y.i in ].a.i,b.i.])
proof
let x be object;
thus x in s iff ex y be Element of REAL n st x = y &
(for i be Nat st i in Seg n holds y.i in ].a.i,b.i.])
proof
hereby
assume
A8: x in s;
then reconsider y = x as Element of REAL n;
take y;
thus x = y;
thus for i be Nat st i in Seg n holds y.i in ].a.i,b.i.]
proof
let i be Nat;
assume
A9: i in Seg n; then
A10: i in dom f by A2,FINSEQ_1:def 3; then
A11: y.i in f.i by A8,CARD_3:9;
consider S2 be Subset of REAL such that
A12: f/.i = S2 and
A13: S2 = ].a.i,b.i.] by A9,A3;
thus y.i in ].a.i,b.i.] by A10,A11,A12,A13,PARTFUN1:def 6;
end;
end;
given y be Element of REAL n such that
A14: x = y and
A15: for i be Nat st i in Seg n holds y.i in ].a.i,b.i.];
now
thus dom y = dom f by A4,FINSEQ_1:89;
thus for z being object st z in dom f holds y.z in f.z
proof
let z be object;
assume
A16: z in dom f; then
A17: z in Seg n by A2,FINSEQ_1:def 3;
then consider S2 be Subset of REAL such that
A18: f/.z = S2 and
A19: S2 = ].a.z,b.z.] by A3;
f/.z = f.z by A16,PARTFUN1:def 6;
hence y.z in f.z by A18,A19,A15,A17;
end;
end;
hence x in s by A14,CARD_3:9;
end;
end;
hence thesis;
end;
uniqueness
proof
let I1,I2 be Subset of REAL n such that
A20: for x being object holds x in I1 iff ex y being Element of REAL n st
x = y &
(for i be Nat st i in Seg n holds y.i in ].a.i,b.i.]) and
A21: for x being object holds x in I2 iff ex y being Element of REAL n st
x = y &
(for i be Nat st i in Seg n holds y.i in ].a.i,b.i.]);
thus I1 c= I2
proof
let x be object;
assume x in I1;
then consider y be Element of REAL n such that
A22: x = y and
A23: for i be Nat st i in Seg n holds y.i in ].a.i,b.i.] by A20;
thus x in I2 by A21,A23,A22;
end;
let x be object;
assume x in I2;
then consider y be Element of REAL n such that
A24: x = y and
A25: for i be Nat st i in Seg n holds y.i in ].a.i,b.i.] by A21;
thus x in I1 by A24,A25,A20;
end;
end;
definition
let n,a,b;
func RightOpenHyperInterval(a,b) -> Subset of REAL n means
:Def6:
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
proof
defpred P[object,object] means ex S be Subset of REAL st
S = $2 & S = [.a.$1,b.$1.[;
A1: for i be Nat st i in Seg n ex d being Element of bool REAL st P[i,d];
consider f being FinSequence of bool REAL such that
A2: len f = n and
A3: for i be Nat st i in Seg n holds P[i,f/.i] from FINSEQ_4:sch 1(A1);
A4: dom f = Seg n by A2,FINSEQ_1:def 3;
set s = product f;
s c= product(Seg n --> REAL)
proof
let t be object;
assume
A5: t in s;
then reconsider t1 = t as Function;
A6: dom t1 = dom f & for y be object st y in dom f holds t1.y in f.y
by A5,CARD_3:9;
now
dom (Seg n --> REAL) = Seg n by FUNCOP_1:13;
hence dom t1 = dom (Seg n --> REAL) by A6,A2,FINSEQ_1:def 3;
thus for y be object st y in dom (Seg n --> REAL) holds
t1.y in (Seg n --> REAL).y
proof
let y be object;
assume
A7: y in dom(Seg n-->REAL);
then y in Seg n;
then y in dom f by A2,FINSEQ_1:def 3;
then t1.y in f.y & f.y in bool REAL by A5,CARD_3:9,FINSEQ_2:11;
then t1.y in REAL;
hence thesis by A7,FUNCOP_1:7;
end;
end;
hence t in product(Seg n --> REAL) by CARD_3:9;
end;
then reconsider s as Subset of REAL n by Th7;
for x being object holds x in s iff ex y be Element of REAL n st
x = y & (for i be Nat st i in Seg n holds y.i in [.a.i,b.i.[)
proof
let x be object;
thus x in s iff ex y be Element of REAL n st x = y &
(for i be Nat st i in Seg n holds y.i in [.a.i,b.i.[)
proof
hereby
assume
A8: x in s;
then reconsider y = x as Element of REAL n;
take y;
thus x = y;
thus for i be Nat st i in Seg n holds y.i in [.a.i,b.i.[
proof
let i be Nat;
assume
A9: i in Seg n; then
A10: i in dom f by A2,FINSEQ_1:def 3; then
A11: y.i in f.i by A8,CARD_3:9;
consider S2 be Subset of REAL such that
A12: f/.i = S2 and
A13: S2 = [.a.i,b.i.[ by A9,A3;
thus y.i in [.a.i,b.i.[ by A10,A11,A12,A13,PARTFUN1:def 6;
end;
end;
given y be Element of REAL n such that
A14: x = y and
A15: for i be Nat st i in Seg n holds y.i in [.a.i,b.i.[;
now
thus dom y = dom f by A4,FINSEQ_1:89;
thus for z being object st z in dom f holds y.z in f.z
proof
let z be object;
assume
A16: z in dom f; then
A17: z in Seg n by A2,FINSEQ_1:def 3;
then consider S2 be Subset of REAL such that
A18: f/.z = S2 and
A19: S2 = [.a.z,b.z.[ by A3;
f/.z = f.z by A16,PARTFUN1:def 6;
hence y.z in f.z by A18,A19,A15,A17;
end;
end;
hence x in s by A14,CARD_3:9;
end;
end;
hence thesis;
end;
uniqueness
proof
let I1,I2 be Subset of REAL n such that
A20: for x being object holds x in I1 iff ex y being Element of REAL n st
x = y &
(for i be Nat st i in Seg n holds y.i in [.a.i,b.i.[) and
A21: for x being object holds x in I2 iff ex y being Element of REAL n st
x = y &
(for i be Nat st i in Seg n holds y.i in [.a.i,b.i.[);
thus I1 c= I2
proof
let x be object;
assume x in I1;
then consider y be Element of REAL n such that
A22: x = y and
A23: for i be Nat st i in Seg n holds y.i in [.a.i,b.i.[ by A20;
thus x in I2 by A21,A23,A22;
end;
thus I2 c= I1
proof
let x be object;
assume x in I2;
then consider y be Element of REAL n such that
A24: x = y and
A25: for i be Nat st i in Seg n holds y.i in [.a.i,b.i.[ by A21;
thus x in I1 by A24,A25,A20;
end;
end;
end;
theorem Th48:
ClosedHyperInterval(a,a) = {a}
proof
A1: ClosedHyperInterval(a,a) c= {a}
proof
let x be object;
assume x in ClosedHyperInterval(a,a);
then consider y be Element of REAL n such that
A2: x = y and
A3: for i be Nat st i in Seg n holds y.i in [.a.i,a.i.] by Def3;
reconsider y1 = y,a1 = a as Function;
A4: dom y = Seg n & dom a1 = Seg n by FINSEQ_2:124;
for z be object st z in dom y1 holds y1.z = a1.z
proof
let z be object;
assume z in dom y1;
then z in Seg n by FINSEQ_2:124;
then y1.z in [.a.z,a.z.] by A3;
then y1.z in {a.z} by XXREAL_1:17;
hence thesis by TARSKI:def 1;
end;
then y1 = a1 by A4,FUNCT_1:def 11;
hence thesis by A2,TARSKI:def 1;
end;
{a} c= ClosedHyperInterval(a,a)
proof
let x be object;
assume
A5: x in {a};
then reconsider x1 = x as Element of REAL n by TARSKI:def 1;
for i be Nat st i in Seg n holds x1.i in [.a.i,a.i.]
proof
let i be Nat;
assume i in Seg n;
x1.i = a.i by A5,TARSKI:def 1;
then x1.i in {a.i} by TARSKI:def 1;
hence thesis by XXREAL_1:17;
end;
hence thesis by Def3;
end;
hence thesis by A1;
end;
registration
let n,a;
cluster ClosedHyperInterval(a,a) -> trivial;
coherence
proof
ClosedHyperInterval(a,a) = {a} by Th48;
hence thesis;
end;
end;
theorem
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
thus OpenHyperInterval(a,b) c= LeftOpenHyperInterval(a,b)
proof
let x be object;
assume x in OpenHyperInterval(a,b);
then consider y be Element of REAL n such that
A1: x = y and
A2: for i be Nat st i in Seg n holds y.i in ].a.i,b.i.[ by Def4;
now
let i be Nat;
assume i in Seg n;
then y.i in ].a.i,b.i.[ & ].a.i,b.i.[ c= ].a.i,b.i.] by A2,XXREAL_1:21;
hence y.i in ].a.i,b.i.];
end;
hence thesis by A1,Def5;
end;
thus OpenHyperInterval(a,b) c= RightOpenHyperInterval(a,b)
proof
let x be object;
assume x in OpenHyperInterval(a,b);
then consider y be Element of REAL n such that
A3: x = y and
A4: for i be Nat st i in Seg n holds y.i in ].a.i,b.i.[ by Def4;
now
let i be Nat;
assume i in Seg n;
then y.i in ].a.i,b.i.[ & ].a.i,b.i.[ c= [.a.i,b.i.[ by A4,XXREAL_1:22;
hence y.i in [.a.i,b.i.[;
end;
hence thesis by A3,Def6;
end;
thus LeftOpenHyperInterval(a,b) c= ClosedHyperInterval(a,b)
proof
let x be object;
assume x in LeftOpenHyperInterval(a,b);
then consider y be Element of REAL n such that
A5: x = y and
A6: for i be Nat st i in Seg n holds y.i in ].a.i,b.i.] by Def5;
now
let i be Nat;
assume i in Seg n;
then y.i in ].a.i,b.i.] & ].a.i,b.i.] c= [.a.i,b.i.] by A6,XXREAL_1:23;
hence y.i in [.a.i,b.i.];
end;
hence thesis by A5,Def3;
end;
thus RightOpenHyperInterval(a,b) c= ClosedHyperInterval(a,b)
proof
let x be object;
assume x in RightOpenHyperInterval(a,b);
then consider y be Element of REAL n such that
A7: x = y and
A8: for i be Nat st i in Seg n holds y.i in [.a.i,b.i.[ by Def6;
now
let i be Nat;
assume i in Seg n;
then y.i in [.a.i,b.i.[ & [.a.i,b.i.[ c= [.a.i,b.i.] by A8,XXREAL_1:24;
hence y.i in [.a.i,b.i.];
end;
hence thesis by A7,Def3;
end;
end;
definition
let n,a,b;
pred a <= b means for i being Nat st i in Seg n holds a.i <= b.i;
reflexivity;
end;
theorem
a <= b & b <= c implies a <= c
proof
assume that
A1: a <= b and
A2: b <= c;
for i be Nat st i in Seg n holds a.i <= c.i
proof
let i be Nat;
assume i in Seg n;
then a.i <= b.i & b.i <= c.i by A1,A2;
hence thesis by XXREAL_0:2;
end;
hence thesis;
end;
theorem Th49:
a <= c & d <= b implies ClosedHyperInterval(c,d) c= ClosedHyperInterval(a,b)
proof
assume that
A1: a <= c and
A3: d <= b;
now
let t be object;
assume t in ClosedHyperInterval(c,d);
then consider t1 be Element of REAL n such that
A4: t = t1 and
A5: for i be Nat st i in Seg n holds t1.i in [.c.i,d.i.] by Def3;
for i be Nat st i in Seg n holds t1.i in [.a.i,b.i.]
proof
let i be Nat;
assume
A6: i in Seg n;
then a.i <= c.i & d.i <= b.i by A1,A3;
then [.c.i,d.i.] c= [.a.i,b.i.] by XXREAL_1:34;
hence thesis by A6,A5;
end;
hence t in ClosedHyperInterval(a,b) by A4,Def3;
end;
hence thesis;
end;
theorem
a <= b implies ClosedHyperInterval(a,b) is non empty
proof
assume a <= b; then
ClosedHyperInterval(a,a) c= ClosedHyperInterval(a,b) by Th49;
then {a} c= ClosedHyperInterval(a,b) by Th48;
hence thesis;
end;
definition
let n,a,b;
pred a < b means for i being Nat st i in Seg n holds a.i < b.i;
end;
theorem
a < b & b < c implies a < c
proof
assume that
A1: a < b and
A2: b < c;
for i be Nat st i in Seg n holds a.i < c.i
proof
let i be Nat;
assume i in Seg n;
then a.i < b.i & b.i < c.i by A1,A2;
hence thesis by XXREAL_0:2;
end;
hence thesis;
end;
theorem
b < a & n is non zero implies ClosedHyperInterval(a,b) is empty
proof
assume that
A1: b < a and
A2: n is non zero;
assume not ClosedHyperInterval(a,b) is empty;
then consider x be object such that
A3: x in ClosedHyperInterval(a,b);
consider y be Element of REAL n such that
x = y and
A4: for i be Nat st i in Seg n holds y.i in [.a.i,b.i.] by A3,Def3;
1 <= n by A2,NAT_1:14;
then b.1 < a.1 & y.1 in [.a.1,b.1.] by A1,A4,FINSEQ_1:1;
hence contradiction by XXREAL_1:29;
end;
theorem Th50:
n|-> r is Element of REAL n
proof
A1: r is Element of REAL by XREAL_0:def 1;
set f = n|-> r;
reconsider f as Function;
f in Funcs(Seg n,REAL)
proof
f is Element of n-tuples_on REAL by A1,FINSEQ_2:112;
then f in n-tuples_on REAL;
hence thesis by FINSEQ_2:93;
end;
hence thesis by FINSEQ_2:93;
end;
definition
let n,r;
redefine func n |-> r -> Element of REAL n; :: redefines |-> (FINSEQ_2, definition)
coherence by Th50;
end;
definition
let r;
redefine func <*r*> -> Element of REAL 1; :: redefines <* (FINSEQ_1, definition)
coherence
proof
1 |-> r is Element of REAL 1;
hence thesis by FINSEQ_2:59;
end;
end;
theorem Th51:
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))
proof
let n be non zero Nat, e be Point of Euclid n;
reconsider a = e as Element of REAL n;
reconsider p = e as Point of TOP-REAL n by EUCLID:67;
consider e0 be Point of Euclid n such that
A1: p = e0 and
A2: OpenHypercube(e0,r) = OpenHypercube(p,r) by TIETZE_2:def 1;
take a;
thus a = e;
A3: OpenHypercube(e,r) c= OpenHyperInterval(a - (n |-> r),a + (n |-> r))
proof
let x be object;
assume
A4: x in OpenHypercube(e,r);
then reconsider y = x as Element of REAL n;
for i be Nat st i in Seg n holds y.i in ].(a-(n|->r)).i,(a+(n|->r)).i.[
proof
let i be Nat;
assume
A5: i in Seg n;
A6: (a - (n|->r)).i = a.i - (n|->r).i by RVSUM_1:27 .= a.i - r
by A5,FINSEQ_2:57;
(a + (n|->r)).i = a.i + (n|->r).i by RVSUM_1:11 .= a.i + r
by A5,FINSEQ_2:57;
hence thesis by A5,A6,A1,A2,A4,TIETZE_2:4;
end;
hence thesis by Def4;
end;
OpenHyperInterval(a - (n|->r),a + (n|->r)) c= OpenHypercube(e,r)
proof
let x be object;
assume
A7: x in OpenHyperInterval(a-(n|->r),a+(n|->r));
then reconsider q = x as Element of TOP-REAL n by EUCLID:22;
now
let i be Nat;
assume
A8: i in Seg n;
consider y being Element of REAL n such that
A9: x = y and
A10: (for i being Nat st i in Seg n holds
y.i in ].(a-(n|->r)).i,(a+(n|->r)).i.[) by A7,Def4;
A11: (a - (n|->r)).i = a.i - (n|->r).i by RVSUM_1:27
.= a.i - r by A8,FINSEQ_2:57;
(a + (n|->r)).i = a.i + (n|->r).i by RVSUM_1:11
.= a.i + r by A8,FINSEQ_2:57;
hence q.i in ].p.i-r,p.i+r.[ by A11,A8,A9,A10;
end;
hence thesis by A1,A2,TIETZE_2:4;
end;
hence thesis by A3;
end;
theorem Th52:
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
let p be Point of TOP-REAL n;
reconsider a = p as Element of REAL n by EUCLID:22;
take a;
thus a = p;
A1: ClosedHypercube(p,b) c= ClosedHyperInterval(a - b,a + b)
proof
let x be object;
assume
A2: x in ClosedHypercube(p,b);
then reconsider y = x as Element of REAL n by EUCLID:22;
for i be Nat st i in Seg n holds y.i in [.(a-b).i,(a+b).i.]
proof
let i be Nat;
assume
A3: i in Seg n;
a.i - b.i = (a - b).i & (a + b).i = a.i + b.i by RVSUM_1:11,RVSUM_1:27;
hence thesis by A2,A3,TIETZE_2:def 2;
end;
hence thesis by Def3;
end;
ClosedHyperInterval(a - b,a + b) c= ClosedHypercube(p,b)
proof
let x be object;
assume
A4: x in ClosedHyperInterval(a-b,a+b);
then reconsider q = x as Element of TOP-REAL n by EUCLID:22;
now
let i be Nat;
assume
A5: i in Seg n;
consider y being Element of REAL n such that
A6: x = y and
A7: (for i being Nat st i in Seg n holds y.i in [.(a-b).i,(a+b).i.])
by A4,Def3;
(a-b).i = a.i-b.i & (a+b).i = a.i+b.i by RVSUM_1:11,RVSUM_1:27;
hence q.i in [.p.i-b.i,p.i+b.i.] by A5,A6,A7;
end;
hence thesis by TIETZE_2:def 2;
end;
hence thesis by A1;
end;
begin :: Correspondance between Interval and 1-dimensional HyperInterval
theorem
for x being Real holds x in [.r,s.] iff
1 |-> x in ClosedHyperInterval(<*r*>,<*s*>)
proof
set a1 = <*r*>, b1 = <*s*>;
A1: for x be Real st x in [.r,s.] holds 1|-> x in ClosedHyperInterval(a1,b1)
proof
let t be Real;
assume
A2: t in [.r,s.];
reconsider t1 = 1|-> t as Element of REAL 1;
ex y be Element of REAL 1 st
t1 = y & (for i be Nat st i in Seg 1 holds y.i in [.a1.i,b1.i.])
proof
take t1;
thus t1 = t1;
thus for i be Nat st i in Seg 1 holds t1.i in [.a1.i,b1.i.]
proof
let i be Nat;
assume
A3: i in Seg 1; then
A4: i = 1 by FINSEQ_1:2,TARSKI:def 1;
now
t1.1 = (Seg 1 --> t).1 by FINSEQ_2:def 2;
hence t1.i = t by A3,A4,FUNCOP_1:7;
thus a1.i = r & b1.i = s by A4;
end;
hence thesis by A2;
end;
end;
hence thesis by Def3;
end;
for x be Real st 1 |-> x in ClosedHyperInterval(a1,b1) holds x in [.r,s.]
proof
let x be Real;
assume 1 |-> x in ClosedHyperInterval(a1,b1);
then consider y be Element of REAL 1 such that
A5: 1 |-> x = y and
A6: for i be Nat st i in Seg 1 holds y.i in [.a1.i,b1.i.] by Def3;
A7: 1 in Seg 1;
y = Seg 1 --> x & 1 in Seg 1 by A5,FINSEQ_2:def 2; then
A8: y.1 = x by FUNCOP_1:7;
a1.1 = r & b1.1 = s;
hence thesis by A6,A7,A8;
end;
hence thesis by A1;
end;
theorem
for x being Real holds x in ].r,s.[ iff
1 |-> x in OpenHyperInterval(<*r*>,<*s*>)
proof
set a1 = <*r*>, b1 = <*s*>;
A1: for x be Real st x in ].r,s.[ holds 1|-> x in OpenHyperInterval(a1,b1)
proof
let t be Real;
assume
A2: t in ].r,s.[;
reconsider t1 = 1|-> t as Element of REAL 1;
ex y be Element of REAL 1 st
t1 = y & (for i be Nat st i in Seg 1 holds y.i in ].a1.i,b1.i.[)
proof
take t1;
thus t1 = t1;
thus for i be Nat st i in Seg 1 holds t1.i in ].a1.i,b1.i.[
proof
let i be Nat;
assume
A3: i in Seg 1; then
A4: i = 1 by FINSEQ_1:2,TARSKI:def 1;
now
t1.1 = (Seg 1 --> t).1 by FINSEQ_2:def 2;
hence t1.i = t by A3,A4,FUNCOP_1:7;
thus a1.i = r & b1.i = s by A4;
end;
hence thesis by A2;
end;
end;
hence thesis by Def4;
end;
for x be Real st 1 |-> x in OpenHyperInterval(a1,b1) holds x in ].r,s.[
proof
let x be Real;
assume 1 |-> x in OpenHyperInterval(a1,b1);
then consider y be Element of REAL 1 such that
A5: 1 |-> x = y and
A6: for i be Nat st i in Seg 1 holds y.i in ].a1.i,b1.i.[ by Def4;
A7: 1 in Seg 1;
y = Seg 1 --> x & 1 in Seg 1 by A5,FINSEQ_2:def 2; then
A8: y.1 = x by FUNCOP_1:7;
a1.1 = r & b1.1 = s;
hence thesis by A6,A7,A8;
end;
hence thesis by A1;
end;
theorem
for x being Real holds x in ].r,s.] iff
1 |-> x in LeftOpenHyperInterval(<*r*>,<*s*>)
proof
set a1 = <*r*>, b1 = <*s*>;
A1: for x be Real st x in ].r,s.] holds 1|-> x in LeftOpenHyperInterval(a1,b1)
proof
let t be Real;
assume
A2: t in ].r,s.];
reconsider t1 = 1|-> t as Element of REAL 1;
ex y be Element of REAL 1 st
t1 = y & (for i be Nat st i in Seg 1 holds y.i in ].a1.i,b1.i.])
proof
take t1;
thus t1 = t1;
thus for i be Nat st i in Seg 1 holds t1.i in ].a1.i,b1.i.]
proof
let i be Nat;
assume
A3: i in Seg 1; then
A4: i = 1 by FINSEQ_1:2,TARSKI:def 1;
now
t1.1 = (Seg 1 --> t).1 by FINSEQ_2:def 2;
hence t1.i = t by A3,A4,FUNCOP_1:7;
thus a1.i = r & b1.i = s by A4;
end;
hence thesis by A2;
end;
end;
hence thesis by Def5;
end;
for x be Real st 1 |-> x in LeftOpenHyperInterval(a1,b1) holds x in ].r,s.]
proof
let x be Real;
assume 1 |-> x in LeftOpenHyperInterval(a1,b1);
then consider y be Element of REAL 1 such that
A5: 1 |-> x = y and
A6: for i be Nat st i in Seg 1 holds y.i in ].a1.i,b1.i.] by Def5;
A7: 1 in Seg 1;
y = Seg 1 --> x & 1 in Seg 1 by A5,FINSEQ_2:def 2; then
A8: y.1 = x by FUNCOP_1:7;
a1.1 = r & b1.1 = s;
hence thesis by A6,A7,A8;
end;
hence thesis by A1;
end;
theorem
for x being Real holds x in [.r,s.[ iff
1 |-> x in RightOpenHyperInterval(<*r*>,<*s*>)
proof
set a1 = <*r*>, b1 = <*s*>;
A1: for x be Real st x in [.r,s.[ holds
1|-> x in RightOpenHyperInterval(a1,b1)
proof
let t be Real;
assume
A2: t in [.r,s.[;
reconsider t1 = 1|-> t as Element of REAL 1;
ex y be Element of REAL 1 st
t1 = y & (for i be Nat st i in Seg 1 holds y.i in [.a1.i,b1.i.[)
proof
take t1;
thus t1 = t1;
thus for i be Nat st i in Seg 1 holds t1.i in [.a1.i,b1.i.[
proof
let i be Nat;
assume
A3: i in Seg 1; then
A4: i = 1 by FINSEQ_1:2,TARSKI:def 1;
now
t1.1 = (Seg 1 --> t).1 by FINSEQ_2:def 2;
hence t1.i = t by A3,A4,FUNCOP_1:7;
thus a1.i = r & b1.i = s by A4;
end;
hence thesis by A2;
end;
end;
hence thesis by Def6;
end;
for x be Real st 1 |-> x in RightOpenHyperInterval(a1,b1) holds
x in [.r,s.[
proof
let x be Real;
assume 1 |-> x in RightOpenHyperInterval(a1,b1);
then consider y be Element of REAL 1 such that
A5: 1 |-> x = y and
A6: for i be Nat st i in Seg 1 holds y.i in [.a1.i,b1.i.[ by Def6;
A7: 1 in Seg 1;
y = Seg 1 --> x & 1 in Seg 1 by A5,FINSEQ_2:def 2; then
A8: y.1 = x by FUNCOP_1:7;
a1.1 = r & b1.1 = s;
hence thesis by A6,A7,A8;
end;
hence thesis by A1;
end;
begin :: Correspondence between MeasurableRectangle and Product
reserve n for non zero Nat;
theorem Th53:
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.[
proof
let s be Tuple of n,the_set_of_all_open_real_bounded_intervals;
s in Funcs(Seg n,the_set_of_all_open_real_bounded_intervals) by Th9;
then consider f be Function such that
A1: s = f and
A2: dom f = Seg n and
rng f c= the_set_of_all_open_real_bounded_intervals by FUNCT_2:def 2;
defpred P[object,object] means ex f be Element of [:REAL,REAL:] st
f = $2 & s.$1=].(f`1),(f`2).[;
A3: for i be Nat st i in Seg n ex d be Element of [:REAL,REAL:] st P[i,d]
proof
let i be Nat;
assume i in Seg n;
then s.i in rng s by A1,A2,FUNCT_1:3;
then s.i in the set of all ].a,b.[ where a,b is Real;
then consider a,b be Real such that
A4: s.i = ].a,b.[;
a in REAL & b in REAL by XREAL_0:def 1;
then reconsider d = [a,b] as Element of [:REAL,REAL:]
by ZFMISC_1:def 2;
take d;
s.i = ].(d`1),(d`2).[ by A4;
hence thesis;
end;
consider f being FinSequence of [:REAL,REAL:] such that
A5: len f = n and
A6: for i being Nat st i in Seg n holds P[i,f/.i] from FINSEQ_4:sch 1(A3);
reconsider f as n-element FinSequence of [:REAL,REAL:]
by A5,CARD_1:def 7;
consider z be Element of [:REAL n,REAL n:] such that
A7: for i being Nat st i in Seg n holds
(z`1).i = (f/.i)`1 & (z`2).i = (f/.i)`2 by Th13;
reconsider a = z`1,b = z`2 as Element of REAL n;
take a,b;
thus for i being Nat st i in Seg n holds s.i = ]. a.i,b.i .[
proof
let i be Nat;
assume i in Seg n;
then a.i = (f/.i)`1 & b.i = (f/.i)`2 & P[i,f/.i] by A6,A7;
hence s.i = ].a.i,b.i.[;
end;
end;
theorem
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 .[)))
proof
let x be Element of Product(n,the_set_of_all_open_real_bounded_intervals);
consider s being Tuple of n,the_set_of_all_open_real_bounded_intervals
such that
A1: 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 by Th42;
consider a,b being Element of REAL n such that
A2: for i being Nat st i in Seg n holds s.i = ].a.i,b.i.[ by Th53;
take a,b;
for t being Element of REAL n holds t in x iff
(for i be Nat st i in Seg n holds t.i in ].a.i,b.i.[)
proof
let t be Element of REAL n;
hereby
assume
A3: t in x;
thus (for i be Nat st i in Seg n holds t.i in ].a.i,b.i.[)
proof
let i be Nat;
assume
A4: i in Seg n;
then s.i = ].a.i,b.i.[ by A2;
hence t.i in ].a.i,b.i.[ by A1,A3,A4;
end;
end;
assume
A5: (for i be Nat st i in Seg n holds t.i in ].a.i,b.i.[);
for i be Nat st i in Seg n holds t.i in s.i
proof
let i be Nat;
assume
A6: i in Seg n;
then s.i = ].a.i,b.i.[ by A2;
hence t.i in s.i by A6,A5;
end;
hence t in x by A1;
end;
hence thesis;
end;
theorem Th54:
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.]
proof
let s be Tuple of n,the_set_of_all_left_open_real_bounded_intervals;
s in Funcs(Seg n,the_set_of_all_left_open_real_bounded_intervals) by Th9;
then consider f be Function such that
A1: s = f and
A2: dom f = Seg n and
rng f c= the_set_of_all_left_open_real_bounded_intervals by FUNCT_2:def 2;
defpred P[object,object] means ex f be Element of [:REAL,REAL:] st
f = $2 & s.$1=].(f`1),(f`2).];
A3: for i be Nat st i in Seg n ex d be Element of [:REAL,REAL:] st P[i,d]
proof
let i be Nat;
assume i in Seg n;
then s.i in rng s by A1,A2,FUNCT_1:3;
then s.i in the set of all ].a,b.] where a,b is Real;
then consider a,b be Real such that
A4: s.i = ].a,b.];
a in REAL & b in REAL by XREAL_0:def 1;
then reconsider d = [a,b] as Element of [:REAL,REAL:]
by ZFMISC_1:def 2;
take d;
s.i = ].(d`1),(d`2).] by A4;
hence thesis;
end;
consider f being FinSequence of [:REAL,REAL:] such that
A5: len f = n and
A6: for i being Nat st i in Seg n holds P[i,f/.i] from FINSEQ_4:sch 1(A3);
reconsider f as n-element FinSequence of [:REAL,REAL:]
by A5,CARD_1:def 7;
consider z be Element of [:REAL n,REAL n:] such that
A7: for i being Nat st i in Seg n holds
(z`1).i = (f/.i)`1 & (z`2).i = (f/.i)`2 by Th13;
reconsider a = z`1,b = z`2 as Element of REAL n;
take a,b;
thus for i being Nat st i in Seg n holds s.i = ]. a.i,b.i .]
proof
let i be Nat;
assume i in Seg n;
then a.i = (f/.i)`1 & b.i = (f/.i)`2 & P[i,f/.i] by A6,A7;
hence s.i = ].a.i,b.i.];
end;
end;
theorem
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 .])))
proof
let x be Element of
Product(n,the_set_of_all_left_open_real_bounded_intervals);
consider s being Tuple of n,
the_set_of_all_left_open_real_bounded_intervals such that
A1: 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 by Th42;
consider a,b being Element of REAL n such that
A2: for i being Nat st i in Seg n holds s.i = ].a.i,b.i.] by Th54;
take a,b;
for t being Element of REAL n holds t in x iff
(for i be Nat st i in Seg n holds t.i in ].a.i,b.i.])
proof
let t be Element of REAL n;
hereby
assume
A3: t in x;
thus (for i be Nat st i in Seg n holds t.i in ].a.i,b.i.])
proof
let i be Nat;
assume
A4: i in Seg n;
then s.i = ].a.i,b.i.] by A2;
hence t.i in ].a.i,b.i.] by A1,A3,A4;
end;
end;
assume
A5: (for i be Nat st i in Seg n holds t.i in ].a.i,b.i.]);
for i be Nat st i in Seg n holds t.i in s.i
proof
let i be Nat;
assume
A6: i in Seg n;
then s.i = ].a.i,b.i.] by A2;
hence t.i in s.i by A6,A5;
end;
hence t in x by A1;
end;
hence thesis;
end;
theorem Th55:
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.[
proof
let s be Tuple of n,the_set_of_all_right_open_real_bounded_intervals;
s in Funcs(Seg n,the_set_of_all_right_open_real_bounded_intervals) by Th9;
then consider f be Function such that
A1: s = f and
A2: dom f = Seg n and
rng f c= the_set_of_all_right_open_real_bounded_intervals by FUNCT_2:def 2;
defpred P[object,object] means ex f be Element of [:REAL,REAL:] st
f = $2 & s.$1=[.(f`1),(f`2).[;
A3: for i be Nat st i in Seg n ex d be Element of [:REAL,REAL:] st P[i,d]
proof
let i be Nat;
assume i in Seg n;
then s.i in rng s by A1,A2,FUNCT_1:3;
then s.i in the set of all [.a,b.[ where a,b is Real;
then consider a,b be Real such that
A4: s.i = [.a,b.[;
a in REAL & b in REAL by XREAL_0:def 1;
then reconsider d = [a,b] as Element of [:REAL,REAL:]
by ZFMISC_1:def 2;
take d;
s.i = [.(d`1),(d`2).[ by A4;
hence thesis;
end;
consider f being FinSequence of [:REAL,REAL:] such that
A5: len f = n and
A6: for i being Nat st i in Seg n holds P[i,f/.i] from FINSEQ_4:sch 1(A3);
reconsider f as n-element FinSequence of [:REAL,REAL:]
by A5,CARD_1:def 7;
consider z be Element of [:REAL n,REAL n:] such that
A7: for i being Nat st i in Seg n holds
(z`1).i = (f/.i)`1 & (z`2).i = (f/.i)`2 by Th13;
reconsider a = z`1,b = z`2 as Element of REAL n;
take a,b;
thus for i being Nat st i in Seg n holds s.i = [. a.i,b.i .[
proof
let i be Nat;
assume i in Seg n;
then a.i = (f/.i)`1 & b.i = (f/.i)`2 & P[i,f/.i] by A6,A7;
hence s.i = [.a.i,b.i.[;
end;
end;
theorem
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 .[)))
proof
let x be Element of
Product(n,the_set_of_all_right_open_real_bounded_intervals);
consider s being Tuple of n,
the_set_of_all_right_open_real_bounded_intervals such that
A1: 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 by Th42;
consider a,b being Element of REAL n such that
A2: for i being Nat st i in Seg n holds s.i = [.a.i,b.i.[ by Th55;
take a,b;
for t being Element of REAL n holds
t in x iff (for i be Nat st i in Seg n holds t.i in [.a.i,b.i.[)
proof
let t be Element of REAL n;
hereby
assume
A3: t in x;
thus (for i be Nat st i in Seg n holds t.i in [.a.i,b.i.[)
proof
let i be Nat;
assume
A4: i in Seg n;
then s.i = [.a.i,b.i.[ by A2;
hence t.i in [.a.i,b.i.[ by A1,A3,A4;
end;
end;
assume
A5: (for i be Nat st i in Seg n holds t.i in [.a.i,b.i.[);
for i be Nat st i in Seg n holds t.i in s.i
proof
let i be Nat;
assume
A6: i in Seg n;
then s.i = [.a.i,b.i.[ by A2;
hence t.i in s.i by A6,A5;
end;
hence t in x by A1;
end;
hence thesis;
end;
theorem
MeasurableRectangle(ProductLeftOpenIntervals(n)) =
Product(n,the_set_of_all_left_open_real_bounded_intervals)
proof
thus MeasurableRectangle(ProductLeftOpenIntervals(n))
c= Product(n,the_set_of_all_left_open_real_bounded_intervals)
proof
let x be object;
assume x in MeasurableRectangle(ProductLeftOpenIntervals(n));
then consider y being Subset of REAL n, a, b being Element of REAL n
such that
A1: x = y and
A2: 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 .]) by Th32;
now
let t being Element of REAL n;
hereby
assume
A3: t in y;
hereby
let i be Nat;
assume
A4: i in Seg n;
consider t0 be Element of REAL n such that
A5: t = t0 and
A6: for i be Nat st i in Seg n holds t0.i in ].a.i,b.i.] by A3,A2;
thus t.i in ].a.i,b.i.] by A6,A4,A5;
end;
end;
assume for i be Nat st i in Seg n holds t.i in ].a.i,b.i.];
hence t in y by A2;
end;
then y is Element of Product(n,
the_set_of_all_left_open_real_bounded_intervals) by Th44;
hence thesis by A1;
end;
thus Product(n,the_set_of_all_left_open_real_bounded_intervals) c=
MeasurableRectangle(ProductLeftOpenIntervals(n))
proof
let x be object;
assume x in Product(n,the_set_of_all_left_open_real_bounded_intervals);
then consider g being Function such that
A7: x = product g and
A8: g in product (Seg n -->
the_set_of_all_left_open_real_bounded_intervals) by Def2;
thus x in MeasurableRectangle(ProductLeftOpenIntervals(n))
by A7,A8,SRINGS_4:def 4;
end;
end;
theorem
MeasurableRectangle(ProductRightOpenIntervals(n)) =
Product(n,the_set_of_all_right_open_real_bounded_intervals)
proof
thus MeasurableRectangle(ProductRightOpenIntervals(n))
c= Product(n,the_set_of_all_right_open_real_bounded_intervals)
proof
let x be object;
assume x in MeasurableRectangle(ProductRightOpenIntervals(n));
then consider y being Subset of REAL n, a, b being Element of REAL n
such that
A1: x = y and
A2: 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 .[) by Th35;
now
let t being Element of REAL n;
hereby
assume
A3: t in y;
hereby
let i be Nat;
assume
A4: i in Seg n;
consider t0 be Element of REAL n such that
A5: t = t0 and
A6: for i be Nat st i in Seg n holds t0.i in [.a.i,b.i.[ by A3,A2;
thus t.i in [.a.i,b.i.[ by A6,A4,A5;
end;
end;
assume for i be Nat st i in Seg n holds t.i in [.a.i,b.i.[;
hence t in y by A2;
end;
then y is Element of
Product(n,the_set_of_all_right_open_real_bounded_intervals)
by Th45;
hence thesis by A1;
end;
thus Product(n,the_set_of_all_right_open_real_bounded_intervals) c=
MeasurableRectangle(ProductRightOpenIntervals(n))
proof
let x be object;
assume x in Product(n,the_set_of_all_right_open_real_bounded_intervals);
then consider g being Function such that
A7: x = product g and
A8: g in product (Seg n -->
the_set_of_all_right_open_real_bounded_intervals) by Def2;
thus x in MeasurableRectangle(ProductRightOpenIntervals(n))
by A7,A8,SRINGS_4:def 4;
end;
end;
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
:Def7:
for x,y being Element of REAL n holds it.(x,y) = sup rng abs(x-y);
existence
proof
deffunc F(Element of REAL n,Element of REAL n)
= In(sup rng abs($1-$2),REAL);
consider f being Function of [:REAL n,REAL n:],REAL such that
A1: for x,y being Element of REAL n holds f.(x,y)=F(x,y) from BINOP_1:sch 4;
take f;
let x,y be Element of REAL n;
dom abs(x-y) is non empty;
then consider a be object such that
A2: a in dom abs(x-y);
(abs(x-y)).a in rng abs(x-y) by A2,FUNCT_1:def 3;
then sup rng abs(x-y) in rng abs(x-y) by XXREAL_2:def 6;
then f.(x,y) = In(sup rng abs(x-y),REAL) & sup rng abs(x-y) in REAL by A1;
hence thesis by SUBSET_1:def 8;
end;
uniqueness
proof
let d1,d2 be Function of [:REAL n,REAL n:],REAL such that
A3: for x,y being Element of REAL n holds d1.(x,y) = sup rng abs(x-y) and
A4: for x,y being Element of REAL n holds d2.(x,y) = sup rng abs(x-y);
now
let x,y be set;
assume that
A5: x in REAL n and
A6: y in REAL n;
reconsider x1 = x,y1 = y as Element of REAL n by A5,A6;
d1.(x1,y1) = sup rng abs(x1-y1) by A3
.= d2.(x1,y1) by A4;
hence d1.(x,y) = d2.(x,y);
end;
hence d1 = d2 by BINOP_1:def 21;
end;
end;
theorem Th56:
(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)
proof
set SA = the set of all |.x.i - y.i.| where i is Element of Seg n;
now
let t be object;
assume t in SA;
then ex i be Element of Seg n st t = |.x.i-y.i.|;
hence t is real;
end;
hence SA is real-membered by MEMBERED:def 3;
A1: SA c= rng abs(x-y)
proof
let t be object;
assume t in SA;
then consider i be Element of Seg n such that
A2: t = |.x.i-y.i.|;
A3: t = |.(x-y).i.| & dom abs(x-y) = Seg n by A2,RVSUM_1:27,FINSEQ_2:124;
reconsider f = (x-y) as complex-valued Function;
t = |.f.|.i by A3,VALUED_1:18;
hence t in rng abs(x-y) by A3,FUNCT_1:def 3;
end;
for t be object st t in rng abs (x-y) holds t in SA
proof
let t be object;
assume t in rng abs (x-y);
then consider i be object such that
A4: i in dom abs (x-y) and
A5: t = (abs (x-y)).i by FUNCT_1:def 3;
A6: i is Element of Seg n by A4,FINSEQ_2:124;
reconsider f = (x-y) as complex-valued Function;
t = |.(x-y).i.| & (x-y).i = x.i - y.i by A4,A5,VALUED_1:18,RVSUM_1:27;
hence thesis by A6;
end;
then rng abs (x-y) c= SA;
hence thesis by A1;
end;
theorem Th57:
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
proof
set S = the set of all |. x.i - y.i .| where i is Element of Seg n;
A1: S is real-membered & S = rng abs (x-y) by Th56;
then reconsider S1 = S as ext-real-membered set;
take S1;
thus thesis by A1,Def7;
end;
theorem Th58:
(Infty_dist n).(x,y) = abs (x-y).max_diff_index(x,y)
proof
max_diff_index(x,y) in dom x by EUCLID_9:4; then
A1: max_diff_index(x,y) in Seg n by FINSEQ_2:124;
dom abs(x-y) = Seg n by FINSEQ_2:124; then
A2: abs(x-y).max_diff_index(x,y) in rng abs(x-y) by A1,FUNCT_1:def 3;
sup rng abs(x-y) is UpperBound of rng abs(x-y) by XXREAL_2:def 3; then
abs(x-y).max_diff_index(x,y) <= sup rng abs(x-y) by A2,XXREAL_2:def 1; then
A3: abs(x-y).max_diff_index(x,y) <= (Infty_dist n).(x,y) by Def7;
(Infty_dist n).(x,y) <= abs(x-y).max_diff_index(x,y)
proof
now
let t be ExtReal;
assume t in rng abs(x-y);
then ex u be object st u in dom abs(x-y) & t = abs(x-y).u
by FUNCT_1:def 3;
hence t <= abs(x-y).max_diff_index(x,y) by EUCLID_9:5;
end;
then abs(x-y).max_diff_index(x,y) is UpperBound of rng abs(x-y)
by XXREAL_2:def 1;
then sup rng abs(x-y) <= abs(x-y).max_diff_index(x,y) by XXREAL_2:def 3;
hence thesis by Def7;
end;
hence thesis by A3,XXREAL_0:1;
end;
theorem Th59:
(Infty_dist n).(x,y) = 0 iff x = y
proof
consider S being ext-real-membered set such that
A1: S = the set of all |. x.i - y.i .| where i is Element of Seg n and
A2: (Infty_dist n).(x,y) = sup S by Th57;
hereby
assume
A3: (Infty_dist n).(x,y) = 0;
A4: dom x = Seg n & dom y = Seg n by FINSEQ_2:124;
now
let i be object;
assume
A5: i in dom x; then
A6: i in Seg n by FINSEQ_2:124;
set AXY = abs(x-y).i;
reconsider f = (x-y) as complex-valued Function;
A7: AXY = |.(x-y).i.| by VALUED_1:18; then
A8: 0 <= AXY by COMPLEX1:46;
AXY = |.x.i - y.i.| by A5,A7,RVSUM_1:27;
then AXY in S by A1,A6;
then abs(x-y).i = 0 by A8,A3,A2,XXREAL_2:4; then
A9: (x-y).i = 0 by A7,ABSVALUE:2;
reconsider rx = x, ry = y as Element of n-tuples_on REAL;
(rx-ry).i = rx.i - ry.i by A5,RVSUM_1:27;
hence x.i = y.i by A9;
end;
hence x = y by A4,FUNCT_1:def 11;
end;
assume
A10: x = y;
S = {0}
proof
for t be object st t in S holds t in {0}
proof
let t be object;
assume t in S;
then consider i be Element of Seg n such that
A11: t = |.x.i-y.i.| by A1;
t = 0 by A11,A10,ABSVALUE:2;
hence t in {0} by TARSKI:def 1;
end; then
A12: S c= {0};
for t be object st t in {0} holds t in S
proof
let t be object;
assume
A13: t in {0};
1 <= 1 & 1 <= n by NAT_1:53;
then 1 is Element of Seg n by FINSEQ_1:1;
then |.x.1 - y.1.| in S & |.x.1 - y.1.| = 0 by A10,ABSVALUE:2,A1;
hence t in S by A13,TARSKI:def 1;
end;
then {0} c= S;
hence thesis by A12;
end;
hence (Infty_dist n).(x,y) = 0 by A2,XXREAL_2:11;
end;
theorem Th60:
(Infty_dist n).(x,y) = (Infty_dist n).(y,x)
proof
(Infty_dist n).(x,y) = sup rng abs(x-y) &
(Infty_dist n).(y,x) = sup rng abs(y-x) by Def7;
hence (Infty_dist n).(x,y) = (Infty_dist n).(y,x) by Th1;
end;
theorem Th61:
(Infty_dist n).(x,y) <= (Infty_dist n).(x,z) + (Infty_dist n).(z,y)
proof
(Infty_dist n).(x,y) in REAL & (Infty_dist n).(x,z) in REAL &
(Infty_dist n).(z,y) in REAL;
then reconsider sxy = sup rng abs(x-y), sxz = sup rng abs(x-z),
szy = sup rng abs(z-y) as Real by Def7;
sxy <= sxz + szy
proof
for er be ExtReal st er in rng abs(x-y) holds er <= sxz + szy
proof
let er be ExtReal;
assume er in rng abs(x-y);
then consider i be object such that
A1: i in dom abs(x-y) and
A2: er = abs(x-y).i by FUNCT_1:def 3;
abs(x-y).i <= sxz + szy
proof
A3: abs(x-y).i <= abs(x-z).i + abs(z-y).i
proof
reconsider fxy = x-y,fxz = x - z,
fzy = z - y as complex-valued Function;
A4: abs fxy.i = |.(x-y).i.| & abs fxz.i = |.(x-z).i.| &
abs fzy.i = |.(z-y).i.| by VALUED_1:18;
|.(x-y).i.| <= |.(x-z).i.| + |.(z-y).i.|
proof
A5: |.(x-y).i.| = |.x.i - y.i.| & |.(x-z).i.| = |.x.i-z.i.| &
|.(z-y).i.| = |.z.i-y.i.| by A1,RVSUM_1:27;
|.(x.i - z.i) + (z.i - y.i).| <= |.x.i-z.i.| + |.z.i-y.i.|
by COMPLEX1:56;
hence thesis by A5;
end;
hence thesis by A4;
end;
abs(x-z).i + abs(z-y).i <= sxz + szy
proof
A6: dom abs(x-z) = Seg n & dom abs (z-y) = Seg n & dom abs(x-y) = Seg n
by FINSEQ_2:124;
abs(x-z).i in rng abs(x-z) & abs(z-y).i in rng abs(z-y)
by A6,A1,FUNCT_1:def 3; then
A7: abs(x-z).i <= sup rng abs(x-z) & abs(z-y).i <= sup rng abs (z-y)
by XXREAL_2:4;
abs(x-z).i in REAL & abs(z-y).i in REAL by A1,A6,Th2; then
abs(x-z).i + abs(z-y).i <= sup rng abs(x-z) + sup rng abs (z-y)
by Th3,A7;
hence thesis by XXREAL_3:def 2;
end;
hence thesis by A3,XXREAL_0:2;
end;
hence thesis by A2;
end;
then sxz + szy is UpperBound of rng abs(x-y) by XXREAL_2:def 1;
hence thesis by XXREAL_2:def 3;
end;
then sxy <= sxz + (Infty_dist n).(z,y) by Def7;
then sxy <= (Infty_dist n).(x,z) + (Infty_dist n).(z,y) by Def7;
hence thesis by Def7;
end;
theorem Th62:
Infty_dist n is_metric_of REAL n
proof
for x,y,z be Element of REAL n holds
((Infty_dist n).(x,y) = 0 iff x = y) &
((Infty_dist n).(x,y) = (Infty_dist n).(y,x)) &
((Infty_dist n).(x,z) <= (Infty_dist n).(x,y) + (Infty_dist n).(y,z))
by Th59,Th60,Th61;
hence thesis by PCOMPS_1:def 6;
end;
theorem Th63:
(Pitag_dist 2).(|[0,0]|,|[1,1]|) = sqrt 2
proof
reconsider A = |[0,0]|,B=|[1,1]| as Element of REAL 2 by EUCLID:22;
|[0,0]|`1 = 0 & |[0,0]|`2 = 0 & |[1,1]|`1 = 1 & |[1,1]|`2 = 1; then
A1: (A-B).1 = 0 - 1 & (A-B).2 = 0 - 1 by RVSUM_1:27;
reconsider f = A-B as FinSequence of REAL;
len f = len(A-B) & len(A-B) = 2 by FINSEQ_2:132; then
A2: |.A-B.| = sqrt ((-1)^2+((-1)^2)) by A1,EUCLID_3:22;
(-1)^2 = 1^2 by SQUARE_1:3 .= 1 * 1 by SQUARE_1:def 1 .= 1;
hence thesis by A2,EUCLID:def 6;
end;
theorem Th64:
(Infty_dist 2).(|[0,0]|,|[1,1]|) = 1
proof
2 is non zero Nat & |[0,0]| is Element of REAL 2 &
|[1,1]| is Element of REAL 2 by EUCLID:22;
then consider S being ext-real-membered set such that
A1: S = the set of all |. |[0,0]|.i - |[1,1]|.i .| where
i is Element of Seg 2 and
A2: (Infty_dist 2).(|[0,0]|,|[1,1]|) = sup S by Th57;
S = {|. 0 - 1 .|}
proof
for t be object st t in S holds t in {|.0-1.|}
proof
let t be object;
assume t in S;
then consider i be Element of Seg 2 such that
A3: t = |.|[0,0]|.i-|[1,1]|.i.| by A1;
per cases by FINSEQ_1:2,TARSKI:def 2;
suppose
A4: i = 1;
thus thesis by TARSKI:def 1,A4,A3;
end;
suppose
A5: i = 2;
thus thesis by TARSKI:def 1,A5,A3;
end;
end; then
A6: S c= {|.0-1.|};
{|.0 - 1.|} c= S
proof
1 in Seg 2;
then |.|[0,0]|.1 - |[1,1]|.1.| in S by A1;
hence thesis by TARSKI:def 1;
end;
hence thesis by A6;
end;
then S = {|. -1 .|} & |.-1.| = - (-1) by ABSVALUE:def 1;
hence thesis by A2,XXREAL_2:11;
end;
theorem Th65:
for x,y being Element of REAL 1 holds (Infty_dist 1).(x,y) = |.x.1-y.1.|
proof
let x,y be Element of REAL 1;
consider S being ext-real-membered set such that
A1: S = the set of all |. x.i - y.i .| where i is Element of Seg 1 and
A2: (Infty_dist 1).(x,y) = sup S by Th57;
S = {|. x.1 - y.1 .|}
proof
for t be object st t in S holds t in {|.x.1-y.1.|}
proof
let t be object;
assume t in S;
then consider i be Element of Seg 1 such that
A3: t = |.x.i-y.i.| by A1;
i = 1 by TARSKI:def 1,FINSEQ_1:2;
hence thesis by A3,TARSKI:def 1;
end; then
A4: S c= {|.x.1-y.1.|};
for t be object st t in {|.x.1-y.1.|} holds t in S
proof
let t be object;
assume t in {|.x.1-y.1.|}; then
A5: t = |.x.1-y.1.| by TARSKI:def 1;
1 is Element of Seg 1 by TARSKI:def 1,FINSEQ_1:2;
hence thesis by A5,A1;
end;
then {|.x.1-y.1.|} c= S;
hence thesis by A4;
end;
hence thesis by A2,XXREAL_2:11;
end;
theorem Th66:
for x,y being Element of REAL 1 holds (Pitag_dist 1).(x,y) = |.x.1-y.1.|
proof
let x,y be Element of REAL 1;
A1: (Pitag_dist 1).(x,y) = |.x-y.| by EUCLID:def 6;
reconsider f = x - y as Element of TOP-REAL 1 by EUCLID:22;
consider r being Real such that
A2: f = <*r*> by JORDAN2B:20;
sqr (x-y) = <*r^2*> by A2,RVSUM_1:55;
then Sum sqr (x-y) = r^2 by RVSUM_1:73; then
A3: sqrt Sum sqr (x-y) = |.r.| by COMPLEX1:72;
f.1 = (x-y).1 = x.1 - y.1 by RVSUM_1:27;
hence thesis by A1,A3,A2;
end;
theorem
Pitag_dist 1 = Infty_dist 1
proof
now
let x,y being set;
assume x in REAL 1 & y in REAL 1;
then reconsider x1 = x, y1 = y as Element of REAL 1;
thus (Pitag_dist 1).(x,y) = |.x1.1-y1.1.| by Th66
.= (Infty_dist 1).(x,y) by Th65;
end;
hence thesis by BINOP_1:def 21;
end;
theorem
Pitag_dist 2 <> Infty_dist 2
proof
set x = |[0,0]|, y = |[1,1]|;
now
take x,y;
x is Element of REAL 2 & y is Element of REAL 2 by EUCLID:22;
hence x in REAL 2 & y in REAL 2;
thus (Pitag_dist 2).(x,y) <> (Infty_dist 2).(x,y)
by Th63,Th64,SQUARE_1:19;
end;
hence thesis;
end;
definition
let n being non zero Nat;
func EMINFTY n -> strict MetrSpace equals MetrStruct(#REAL n,Infty_dist n#);
coherence
proof
SpaceMetr(REAL n,Infty_dist n) = MetrStruct(#REAL n,Infty_dist n#)
by Th62,PCOMPS_1:def 7;
hence thesis;
end;
end;
registration
let n being non zero Nat;
cluster EMINFTY n -> non empty;
coherence;
end;
definition
let n being non zero Nat;
func TOP-REAL-INFTY n -> strict RLTopStruct means
:Def8:
the TopStruct of it = TopSpaceMetr EMINFTY n &
the RLSStruct of it = RealVectSpace Seg n;
existence
proof
set V = RealVectSpace Seg n,
T = TopSpaceMetr EMINFTY n;
the topology of T c= bool the carrier of V
proof
let t be object;
assume t in the topology of T;
then t in bool REAL n & REAL n = Funcs(Seg n,REAL) by FINSEQ_2:93;
hence t in bool the carrier of V;
end;
then reconsider t = the topology of T as Subset-Family of the carrier of V;
take S = RLTopStruct(# the carrier of V,
the ZeroF of V,
the addF of V,
the Mult of V,
t #);
thus the TopStruct of S = TopSpaceMetr EMINFTY n by FINSEQ_2:93;
thus the RLSStruct of S = RealVectSpace Seg n;
end;
uniqueness;
end;
theorem
the RLSStruct of TOP-REAL n = the RLSStruct of TOP-REAL-INFTY n
proof
the RLSStruct of TOP-REAL n = RealVectSpace Seg n by EUCLID:def 8;
hence thesis by Def8;
end;
registration
let n being non zero Nat;
cluster TOP-REAL-INFTY n -> non empty;
coherence proof
the TopStruct of TOP-REAL-INFTY n = TopSpaceMetr EMINFTY n by Def8;
hence thesis;
end;
end;
theorem
for x being Element of REAL 0 holds Intervals(x,r) is empty &
product Intervals(x,r) = {{}} by CARD_3:10;
theorem Th67:
r <= 0 implies product Intervals(x,r) is empty
proof
assume
A1: r <= 0;
assume product Intervals(x,r) is non empty;
then consider t be object such that
A2: t in product Intervals(x,r);
consider g be Function such that
g = t and
dom g = dom Intervals(x,r) and
A3: for y being object st y in dom Intervals(x,r) holds g.y in Intervals(x,r).y
by A2,CARD_3:def 5;
A4: dom x = Seg n by FINSEQ_2:124; then
A5: dom Intervals(x,r) = Seg n by EUCLID_9:def 3;
A6: n = 1 or n > 1 by NAT_1:53;
then 1 in dom Intervals(x,r) by A5;
then g.1 in Intervals(x,r).1 & 1 in dom x by A3,A4,A6;
then ].x.1-r,x.1+r.[ is non empty by EUCLID_9:def 3;
hence contradiction by A1;
end;
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 p;
coherence;
end;
theorem Th68:
Ball(p,r) = product Intervals(@p,r)
proof
consider x be Element of REAL n such that
A1: @p = x;
per cases;
suppose r <= 0;
then Ball(p,r) = {} & product Intervals(x,r) = {} by Th67,TBSP_1:12;
hence thesis by A1;
end;
suppose
A2: r > 0;
A3: {q where q is Element of EMINFTY n : dist(p,q) < r} c=
product Intervals(x,r)
proof
let t be object;
assume t in {q where q is Element of EMINFTY n : dist(p,q) < r};
then consider q be Element of EMINFTY n such that
A4: t = q and
A5: dist(p,q) < r;
reconsider pr = p, qr = q as Element of REAL n;
consider S being
ext-real-membered set such that
A6: S = the set of all |. pr.i - qr.i .| where i is Element of Seg n and
A7: (Infty_dist n).(pr,qr) = sup S by Th57;
(Infty_dist n).(p,q) in REAL by BINOP_1:17;
then reconsider s = (Infty_dist n).(p,q) as Real;
reconsider f = Intervals(x,r) as Function;
now
A8: dom f = dom x by EUCLID_9:def 3
.= Seg n by FINSEQ_1:89;
hence dom qr = dom f by FINSEQ_1:89;
thus for y being object st y in dom f holds qr.y in f.y
proof
let y be object;
assume
A9: y in dom f; then
A10: y in dom x by A8,FINSEQ_1:89;
reconsider y1 = y as Element of Seg n by A9,A8;
|. pr.y1 - qr.y1 .| in S by A6;
then |. pr.y1 - qr.y1 .| <= sup S & sup S < r by A7,A5,XXREAL_2:4;
then
A11: |.x.y - qr.y.| < r by A1,XXREAL_0:2;
x.y -r < qr.y & qr.y < x.y + r
proof
per cases;
suppose
A12: x.y - qr.y >= 0;
then x.y - qr.y < r by A11,COMPLEX1:43;
then x.y - qr.y +qr.y < qr.y + r by XREAL_1:8;
then x.y - r < qr.y + r - r by XREAL_1:8;
hence x.y - r < qr.y;
0 + qr.y <= x.y -qr.y +qr.y by A12,XREAL_1:7;
hence thesis by A2,XREAL_1:8;
end;
suppose
A13: x.y - qr.y < 0;
then x.y - qr.y + qr.y < 0 + qr.y by XREAL_1:8;
then x.y - r < qr.y - 0 by A2,XREAL_1:15;
hence x.y - r < qr.y;
|.x.y - qr.y.| = -(x.y - qr.y) by A13,COMPLEX1:70
.= qr.y - x.y;
then qr.y - x.y + x.y < r + x.y by A11,XREAL_1:8;
hence qr.y < x.y + r;
end;
end;
then qr.y in ]. x.y - r , x.y + r .[ by XXREAL_1:4;
hence qr.y in f.y by A10,EUCLID_9:def 3;
end;
end;
hence thesis by A4,CARD_3:9;
end;
product Intervals(x,r) c=
{q where q is Element of EMINFTY n : dist(p,q) < r}
proof
let t be object;
assume t in product Intervals(x,r);
then consider g be Function such that
A14: t = g and
A15: dom g = dom Intervals(x,r) and
A16: for y be object st y in dom Intervals(x,r) holds
g.y in (Intervals(x,r)).y by CARD_3:def 5;
A17: dom Intervals(x,r) = dom x by EUCLID_9:def 3
.= Seg n by FINSEQ_1:89;
rng g c= REAL
proof
let u be object;
assume u in rng g;
then consider t be object such that
A18: t in dom g and
A19: u = g.t by FUNCT_1:def 3;
A20: u in (Intervals(x,r)).t by A18,A19,A15,A16;
t in dom x by A18,A17,A15,FINSEQ_1:89;
then u in ].x.t-r,x.t+r.[ by A20,EUCLID_9:def 3;
hence thesis;
end;
then g in Funcs(Seg n,REAL) by A17,A15,FUNCT_2:def 2;
then reconsider g0 = g as Element of EMINFTY n by FINSEQ_2:93;
dist(p,g0) < r
proof
reconsider p1 = p, g1 = g0 as Element of REAL n;
consider S being
ext-real-membered set such that
S = the set of all |. p1.i - g1.i .| where
i is Element of Seg n and
A21: (Infty_dist n).(p1,g1) = sup S by Th57;
sup S < r
proof
assume
A22: r <= sup S;
set md = max_diff_index(p1,g1);
A23: r <= abs (p1-g1).md by A22,A21,Th58;
A24: md in dom x by A1,EUCLID_9:4;
then md in dom Intervals(x,r) by EUCLID_9:def 3;
then g1.md in (Intervals(x,r)).md by A16; then
A25: g1.md in ].p1.md-r,p1.md+r.[ by A24,A1,EUCLID_9:def 3;
A26: p1.md - r < g1.md & g1.md < p1.md + r by A25,XXREAL_1:4;
p1.md - r + r < g1.md + r by A26,XREAL_1:8; then
A27: p1.md - g1.md < g1.md + r - g1.md by XREAL_1:14;
g1.md - p1.md < p1.md + r - p1.md by A26,XREAL_1:14; then
A28: p1.md - g1.md < r & -(p1.md - g1.md) < r by A27; then
A29: (p1 - g1).md < r & -(p1 - g1).md < r by RVSUM_1:27;
set pg = (p1 - g1).md;
|.pg.| < r
proof
per cases;
suppose pg < 0;
then |.pg.| = -pg by COMPLEX1:70;
hence thesis by A28,RVSUM_1:27;
end;
suppose 0 <= pg;
hence thesis by A29,COMPLEX1:43;
end;
end;
hence contradiction by A23,VALUED_1:18;
end;
hence thesis by A21;
end;
hence t in {q where q is Element of EMINFTY n : dist(p,q) < r} by A14;
end;
hence Ball(p,r) = product Intervals(@p,r) by A1,A3,METRIC_1:def 14;
end;
end;
theorem
for e being Point of Euclid n st e = p holds Ball(p,r) = OpenHypercube(e,r)
proof
let e be Point of Euclid n;
assume
A1: e = p;
Ball(p,r) = product Intervals(@p,r) by Th68;
hence thesis by A1;
end;
registration
let n be non zero Nat,
p be Element of EMINFTY n,
r be negative Real;
cluster cl_Ball(p,r) -> empty;
coherence
proof
assume not thesis;
then consider x be object such that
A1: x in cl_Ball(p,r); reconsider x as Element of EMINFTY n by A1;
dist(x,p) <= r by A1,METRIC_1:12;
hence contradiction by METRIC_1:5;
end;
end;
theorem Th69:
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
reconsider x = @p as Element of REAL n;
per cases;
suppose
A1: r < 0;
for t being object st ex f being Function st t = f & dom f = Seg n &
for i being Nat st i in Seg n holds f.i in [.x.i-r,x.i+r.] holds
t in cl_Ball(p,r)
proof
let t be object;
given f be Function such that
t = f and
dom f = Seg n and
A2: for i being Nat st i in Seg n holds f.i in [.x.i-r,x.i+r.];
x.1 + r < x.1 & x.1 < x.1 - r by A1,XREAL_1:30,XREAL_1:46;
then x.1 + r < x.1 - r by XXREAL_0:2; then
A3: [.x.1 - r , x.1 + r .] is empty by XXREAL_1:29;
0+1 < n+1 by XREAL_1:6;
then 1 <= n by NAT_1:13;
then 1 in Seg n;
hence thesis by A3,A2;
end;
hence thesis by A1;
end;
suppose
A4: 0 <= r;
A5: for t be object st t in cl_Ball(p,r) holds ex f be Function st
t = f & dom f = Seg n & for i be Nat st i in Seg n holds
f.i in [.x.i-r,x.i+r.]
proof
let t be object;
assume
A6: t in cl_Ball(p,r);
reconsider f = t as Function by A6;
take f;
thus t = f;
f is Tuple of n,REAL by A6,FINSEQ_2:131;
hence dom f = Seg n by FINSEQ_2:124;
hereby
let i be Nat;
assume
A7: i in Seg n;
reconsider fx = t as Element of EMINFTY n by A6;
A8: dist(fx,p) <= r by A6,METRIC_1:12;
reconsider rfx = fx, rp = p as Element of REAL n;
consider S being ext-real-membered set such that
A9: S = the set of all |. rfx.i - rp.i .| where i is Element of Seg n and
A10: (Infty_dist n).(rfx,rp) = sup S by Th57;
|. rfx.i - rp.i .| in S by A9,A7;
then |. rfx.i - rp.i .| <= sup S by XXREAL_2:4; then
A11: |. rfx.i - rp.i .| <= r by A10,A8,XXREAL_0:2;
set rfp = rfx.i - rp.i;
x.i - r <= rfx.i & rfx.i <= x.i + r
proof
per cases;
suppose
A12: 0 <= rfp;
then rfx.i - rp.i <= r by A11,COMPLEX1:43; then
A13: rfx.i - rp.i + rp.i <= r + rp.i by XREAL_1:7;
0 + rp.i <= rfx.i - rp.i + rp.i by A12,XREAL_1:7;
then rp.i - r <= rfx.i - r & rfx.i - r <= rfx.i
by A4,XREAL_1:13,XREAL_1:43;
hence thesis by A13,XXREAL_0:2;
end;
suppose
A14: rfp < 0;
then -rfp <= r by A11,COMPLEX1:70;
then rp.i - rfx.i + rfx. i <= r + rfx.i by XREAL_1:7;
then rp.i - r <= r + rfx.i - r by XREAL_1:13;
hence x.i -r <= rfx.i;
rfx.i - rp.i + rp.i < 0 + rp.i by A14,XREAL_1:8;
hence thesis by A4,XREAL_1:38;
end;
end;
hence f.i in [.x.i-r,x.i+r.] by XXREAL_1:1;
end;
end;
for t be object st ex f be Function st t = f & dom f = Seg n &
for i be Nat st i in Seg n holds f.i in [.x.i-r,x.i+r.] holds
t in cl_Ball(p,r)
proof
let t be object;
assume
A15: ex f be Function st t = f & dom f = Seg n & for i be Nat st
i in Seg n holds f.i in [.x.i-r,x.i+r.];
then consider f be Function such that
A16: t = f and
A17: dom f = Seg n and
A18: for i be Nat st i in Seg n holds f.i in [.x.i-r,x.i+r.];
rng f c= REAL
proof
let u be object;
assume u in rng f;
then consider v be object such that
A19: v in dom f and
A20: u = f.v by FUNCT_1:def 3;
f.v in [.x.v-r,x.v+r.] by A19,A17,A18;
hence u in REAL by A20;
end;
then f in Funcs(Seg n,REAL) by A17,FUNCT_2:def 2;
then reconsider q = f as Element of EMINFTY n by FINSEQ_2:93;
dist(p,q) <= r
proof
reconsider rp = p,rq = q as Element of REAL n;
consider S being ext-real-membered set such that
A21: S = the set of all |. rp.i - rq.i .| where i is Element of Seg n and
A22: (Infty_dist n).(rp,rq) = sup S by Th57;
for e be ExtReal st e in S holds e <= r
proof
let e be ExtReal;
assume e in S;
then consider i be Element of Seg n such that
A23: e = |.rp.i - rq.i.| by A21;
|.rp.i - rq.i.| <= r
proof
rq.i in [.rp.i-r,rp.i+r.] by A16,A15; then
A24: rp.i - r <= rq.i & rq.i <= rp.i + r by XXREAL_1:1;
set rpq = rp.i - rq.i;
per cases;
suppose
A25: 0 <= rpq;
rpq <= r
proof
rp.i - r + r <= rq.i + r by A24,XREAL_1:7;
then rp.i - rq.i <= rq.i + r - rq.i by XREAL_1:13;
hence thesis;
end;
hence thesis by A25,COMPLEX1:43;
end;
suppose
A26: rpq < 0;
-rpq <= r
proof
rq.i - rp.i <= rp.i + r - rp.i by A24,XREAL_1:13;
hence thesis;
end;
hence thesis by A26,COMPLEX1:70;
end;
end;
hence e <= r by A23;
end;
then r is UpperBound of S by XXREAL_2:def 1;
hence thesis by A22,XXREAL_2:def 3;
end;
hence t in cl_Ball(p,r) by A16,METRIC_1:12;
end;
hence thesis by A5;
end;
end;
theorem Th70:
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)
proof
let p be Point of TOP-REAL n,
q be Element of EMINFTY n;
assume
A1: q = p;
A8: cl_Ball(q,r) c= ClosedHypercube(p,n|->r)
proof
let x be object;
assume x in cl_Ball(q,r);
then consider f being Function such that
A2: x = f and
A3: dom f = Seg n and
A4: for i being Nat st i in Seg n holds f.i in [.(@q).i-r,(@q).i+r.]
by Th69;
reconsider rq = @q as Element of REAL n;
A5: now
let i be Nat;
assume i in Seg n;
then f.i in [.rq.i-r,rq.i+r.] & (n|->r).i = r by A4,FINSEQ_2:57;
hence f.i in [.p.i-(n|->r).i,p.i+(n|->r).i.] by A1;
end;
rng f c= REAL
proof
let u be object;
assume u in rng f;
then consider v be object such that
A6: v in dom f and
A7: u = f.v by FUNCT_1:def 3;
f.v in [.rq.v-r,rq.v+r.] by A6,A3,A4;
hence u in REAL by A7;
end;
then f in Funcs(Seg n,REAL) by A3,FUNCT_2:def 2;
then f in REAL n by FINSEQ_2:93;
then reconsider fx = f as Element of TOP-REAL n by EUCLID:22;
fx in ClosedHypercube(p, n|->r) by A5,TIETZE_2:def 2;
hence thesis by A2;
end;
ClosedHypercube(p,n|->r) c= cl_Ball(q,r)
proof
let x be object;
assume
A9: x in ClosedHypercube(p,n|->r);
then reconsider y = x as Element of TOP-REAL n;
reconsider f = y as Function;
now
take f;
thus y = f;
y in TOP-REAL n;
then y in REAL n by EUCLID:22;
then y is Tuple of n,REAL by FINSEQ_2:131;
hence dom f = Seg n by FINSEQ_2:124;
hereby
let i be Nat;
assume i in Seg n;
then y.i in [.p.i-(n|->r).i,p.i+(n|->r).i.] & (n|->r).i = r
by FINSEQ_2:57,A9,TIETZE_2:def 2;
hence f.i in [.(@q).i-r,(@q).i+r.] by A1;
end;
end;
hence thesis by Th69;
end;
hence thesis by A8;
end;
theorem
Ball(p,r) = OpenHyperInterval(@p - (n|-> r), @p + (n|-> r))
proof
reconsider e = p as Point of Euclid n;
ex a being Element of REAL n st a = e &
OpenHypercube(e,r) = OpenHyperInterval(a - (n|-> r),
a + (n|-> r)) by Th51;
hence thesis by Th68;
end;
theorem
cl_Ball(p,r) = ClosedHyperInterval(@p - (n|-> r), @p + (n|-> r))
proof
reconsider q = p as Point of TOP-REAL n by EUCLID:22;
ex a be Element of REAL n st a = p &
ClosedHypercube(q,n |-> r)
= ClosedHyperInterval(a - (n |-> r),a + (n |-> r)) by Th52;
hence thesis by Th70;
end;