:: The Correspondence Between $n$-dimensional {E}uclidean Space and the
:: Product of $n$ Real Lines
:: by Artur Korni{\l}owicz
::
:: Received November 30, 2009
:: Copyright (c) 2009-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 RELAT_1, FUNCT_1, VALUED_0, ARYTM_1, COMPLEX1, ARYTM_3, XCMPLX_0,
FINSEQ_1, EUCLID, PRE_TOPC, ORDINAL2, METRIC_1, TOPMETR, RCOMP_1,
PCOMPS_1, FINSEQ_2, RVSUM_1, SQUARE_1, FUNCT_4, VALUED_2, SUBSET_1,
FUNCOP_1, PARTFUN1, CARD_3, MONOID_0, CANTOR_1, QC_LANG1, SETFAM_1,
RLVECT_2, WAYBEL18, RLVECT_3, PBOOLE, TOPGEN_2, STRUCT_0, FINSET_1,
FUNCT_2, TARSKI, CARD_1, YELLOW_8, NAT_1, ZFMISC_1, XBOOLE_0, VALUED_1,
NUMBERS, XXREAL_0, XXREAL_1, EUCLID_9, REAL_1, SUPINF_2;
notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, TOPS_2, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, CARD_1, NUMBERS,
VALUED_0, VALUED_1, XCMPLX_0, XREAL_0, XXREAL_0, XXREAL_2, REAL_1,
CARD_3, COMPLEX1, SQUARE_1, CANTOR_1, FUNCOP_1, FINSEQ_1, FINSEQ_2,
RCOMP_1, FUNCT_7, VALUED_2, STRUCT_0, RVSUM_1, MONOID_0, PRE_TOPC,
METRIC_1, PCOMPS_1, TOPMETR, ALGSTR_0, EUCLID, PRALG_1, YELLOW_8,
WAYBEL18, TOPGEN_2, TOPREAL9, TOPREALB;
constructors MONOID_0, FUNCT_7, VALUED_2, TOPREAL9, TOPREALB, COMPLEX1,
SQUARE_1, FUNCSDOM, WAYBEL18, BINOP_2, TOPGEN_2, PCOMPS_1, SEQ_4, REAL_1,
FCONT_1, WAYBEL_8, PARTFUN3, LATTICE3, BORSUK_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, VALUED_0, VALUED_1, MEMBERED,
XCMPLX_0, XREAL_0, VALUED_2, STRUCT_0, EUCLID, MONOID_0, TOPREALB,
XXREAL_0, NAT_1, TOPMETR, RVSUM_1, TOPREAL9, SQUARE_1, PCOMPS_1, RCOMP_1,
FUNCT_7, FINSEQ_1, FUNCOP_1, WAYBEL18, JORDAN2B, SERIES_3, FINSEQ_2,
XXREAL_2, FINSET_1, PARTFUN3, CARD_1, ORDINAL1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
definitions RELAT_1, FINSEQ_1, TOPS_2, CANTOR_1, YELLOW_8, TARSKI, XBOOLE_0,
LATTICE7, CARD_1;
equalities CARD_3, XCMPLX_0, SQUARE_1, VALUED_1, FINSEQ_2, METRIC_1, PCOMPS_1,
TOPMETR, EUCLID, TOPREALB;
expansions MONOID_0, TARSKI, XBOOLE_0, VALUED_2, STRUCT_0;
theorems FUNCT_1, PARTFUN1, FUNCT_2, VALUED_1, FUNCT_7, VALUED_2, TOPMETR,
TOPREAL9, EUCLID, GOBOARD6, METRIC_1, XBOOLE_1, XXREAL_0, XREAL_1,
XBOOLE_0, RCOMP_1, FINSEQ_2, XREAL_0, FRECHET, FINSEQ_1, FUNCOP_1,
PRE_TOPC, SQUARE_1, RVSUM_1, COMPLEX1, XXREAL_1, RELAT_1, XCMPLX_1,
ORDINAL1, MATRPROB, TARSKI, ZFMISC_1, WAYBEL18, FINSEQ_3, CANTOR_1,
XXREAL_2, YELLOW_9, CARD_3, FCONT_3, PRALG_1, PCOMPS_1, SETFAM_1,
TOPGEN_2, RINFSUP1, CARD_1;
schemes FUNCT_1, PBOOLE, PRE_CIRC;
begin
reserve
x, y for object,
i, n for Nat,
r, s for Real,
f1, f2 for n-element real-valued FinSequence;
registration
let s be Real; let r be non positive Real;
cluster ]. s-r , s+r .[ -> empty;
coherence
by XREAL_1:6,XXREAL_1:28;
cluster [. s-r , s+r .[ -> empty;
coherence
by XREAL_1:6,XXREAL_1:27;
cluster ]. s-r , s+r .] -> empty;
coherence
by XREAL_1:6,XXREAL_1:26;
end;
registration
let s be Real; let r be negative Real;
cluster [. s-r , s+r .] -> empty;
coherence
by XREAL_1:6,XXREAL_1:29;
end;
registration
let n; let f be n-element complex-valued FinSequence;
cluster -f -> n-element;
coherence
proof
A1: dom - f = dom f by VALUED_1:8;
len f = n by CARD_1:def 7;
hence len -f = n by A1,FINSEQ_3:29;
end;
cluster f" -> n-element;
coherence
proof
A2: dom(f") = dom f by VALUED_1:def 7;
len f = n by CARD_1:def 7;
hence len(f") = n by A2,FINSEQ_3:29;
end;
cluster f^2 -> n-element;
coherence
proof
A3: dom(f^2) = dom f by VALUED_1:11;
len f = n by CARD_1:def 7;
hence len(f^2) = n by A3,FINSEQ_3:29;
end;
cluster abs f -> n-element;
coherence
proof
A4: dom abs f = dom f by VALUED_1:def 11;
len f = n by CARD_1:def 7;
hence len abs f = n by A4,FINSEQ_3:29;
end;
let g be n-element complex-valued FinSequence;
cluster f + g -> n-element;
coherence
proof
A5: n in NAT by ORDINAL1:def 12;
A6: dom(f+g) = dom f /\ dom g by VALUED_1:def 1;
len f = n & len g = n by CARD_1:def 7;
then dom f = Seg n & dom g = Seg n by FINSEQ_1:def 3;
hence len(f+g) = n by A5,A6,FINSEQ_1:def 3;
end;
cluster f - g -> n-element;
coherence;
cluster f (#) g -> n-element;
coherence
proof
A7: n in NAT by ORDINAL1:def 12;
A8: dom(f(#)g) = dom f /\ dom g by VALUED_1:def 4;
len f = n & len g = n by CARD_1:def 7;
then dom f = Seg n & dom g = Seg n by FINSEQ_1:def 3;
hence len(f(#)g) = n by A7,A8,FINSEQ_1:def 3;
end;
cluster f /" g -> n-element;
coherence;
end;
registration
let c be Complex, n be Nat, f be n-element complex-valued FinSequence;
cluster c + f -> n-element;
coherence
proof
A1: dom(c+f) = dom f by VALUED_1:def 2;
len f = n by CARD_1:def 7;
hence len(c+f) = n by A1,FINSEQ_3:29;
end;
cluster f - c -> n-element;
coherence;
cluster c (#) f -> n-element;
coherence
proof
A2: dom(c(#)f) = dom f by VALUED_1:def 5;
len f = n by CARD_1:def 7;
hence len(c(#)f) = n by A2,FINSEQ_3:29;
end;
end;
registration
let f be real-valued Function;
cluster {f} -> real-functions-membered;
coherence
by TARSKI:def 1;
let g be real-valued Function;
cluster {f,g} -> real-functions-membered;
coherence
by TARSKI:def 2;
end;
registration
let n, x, y; let f be n-element FinSequence;
cluster f+*(x,y) -> n-element;
coherence
proof
dom(f+*(x,y)) = dom f by FUNCT_7:30;
hence len(f+*(x,y)) = len f by FINSEQ_3:29
.= n by CARD_1:def 7;
end;
end;
theorem
for f being n-element FinSequence st f is empty holds n = 0;
theorem
for f being n-element real-valued FinSequence holds f in REAL n
proof
let f be n-element real-valued FinSequence;
rng f c= REAL;
then f is FinSequence of REAL by FINSEQ_1:def 4;
then
A1: f is Element of REAL* by FINSEQ_1:def 11;
len f = n by CARD_1:def 7;
hence thesis by A1;
end;
theorem Th3:
for f, g being complex-valued Function holds abs(f-g) = abs(g-f)
proof
let f, g be complex-valued Function;
f-g = -(g-f) by VALUED_2:18;
hence thesis by EUCLID:5;
end;
definition
let n, f1, f2;
func max_diff_index(f1,f2) -> Nat equals
the Element of abs(f1-f2) " { sup rng abs(f1-f2) };
coherence;
commutativity
proof
let i,f1,f2;
abs(f1-f2) = abs(f2-f1) by Th3;
hence thesis;
end;
end;
theorem
n <> 0 implies max_diff_index(f1,f2) in dom f1
proof
set F = abs(f1-f2);
assume n <> 0;
then F is non empty;
then sup rng F in rng F by XXREAL_2:def 6;
then
A1: F"{sup rng F} <> {} by FUNCT_1:72;
A2: dom f1 = Seg n by FINSEQ_1:89;
A3: dom abs(f1-f2) = Seg n by FINSEQ_1:89;
A4: F"{sup rng F} c= dom F by RELAT_1:132;
max_diff_index(f1,f2) in F"{sup rng F} by A1;
hence thesis by A4,A2,A3;
end;
theorem Th5:
abs(f1-f2).x <= abs(f1-f2).max_diff_index(f1,f2)
proof
set F = abs(f1-f2);
A1: dom F = dom(f1-f2) by VALUED_1:def 11
.= dom f1 /\ dom f2 by VALUED_1:12;
set m = max_diff_index(f1,f2);
A2: dom f1 = Seg n & dom f2 = Seg n by FINSEQ_1:89;
per cases;
suppose x in dom f1;
then
A3: F.x in rng F by A2,A1,FUNCT_1:def 3;
then sup rng F in rng F by XXREAL_2:def 6;
then
F"{sup rng F} <> {} by FUNCT_1:72;
then F.m in {sup rng F} by FUNCT_1:def 7;
then F.m = sup rng F by TARSKI:def 1;
hence thesis by A3,XXREAL_2:4;
end;
suppose not x in dom f1;
then
A4: not x in dom F by A1,XBOOLE_0:def 4;
F.m = |.(f1-f2).m.| by VALUED_1:18;
hence thesis by A4,FUNCT_1:def 2;
end;
end;
registration
cluster TopSpaceMetr Euclid 0 -> trivial;
coherence by EUCLID:77;
end;
registration
let n;
cluster Euclid n -> constituted-FinSeqs;
coherence;
end;
registration
let n;
cluster -> REAL-valued for Point of Euclid n;
coherence;
end;
registration
let n;
cluster -> n-element for Point of Euclid n;
coherence;
end;
theorem Th6:
Family_open_set(Euclid 0) = {{},{{}}}
proof
the TopStruct of TOP-REAL 0 = TopSpaceMetr Euclid 0 by EUCLID:def 8;
hence thesis by EUCLID:77,YELLOW_9:9;
end;
theorem
for B being Subset of Euclid 0 holds B = {} or B = {{}}
by EUCLID:77,ZFMISC_1:33;
reserve e, e1 for Point of Euclid n;
definition
let n, e;
func @e -> Point of TopSpaceMetr Euclid n equals
e;
coherence;
end;
registration
let n, e;
let r be non positive Real;
cluster Ball(e,r) -> empty;
coherence
proof
assume not thesis;
then consider x being Point of Euclid n such that
A1: x in Ball(e,r);
dist(x,e) < r by A1,METRIC_1:11;
hence thesis by METRIC_1:5;
end;
end;
registration
let n, e;
let r be positive Real;
cluster Ball(e,r) -> non empty;
coherence by GOBOARD6:1;
end;
theorem Th8:
for p1, p2 being Point of TOP-REAL n st i in dom p1 holds
(p1/.i - p2/.i)^2 <= Sum sqr (p1-p2)
proof
let p1, p2 be Point of TOP-REAL n such that
A1: i in dom p1;
set e = sqr(p1-p2);
A2: now
let i be Nat such that i in dom e;
e.i = ((p1-p2).i)^2 by VALUED_1:11;
hence 0 <= e.i;
end;
A3: dom e = dom (p1-p2) by VALUED_1:11;
A4: dom (p1-p2) = dom p1 /\ dom p2 by VALUED_1:12;
A5: dom p1 = Seg n by FINSEQ_1:89
.= dom p2 by FINSEQ_1:89;
A6: p1.i = p1/.i by A1,PARTFUN1:def 6;
A7: p2.i = p2/.i by A1,A5,PARTFUN1:def 6;
e.i = ((p1-p2).i)^2 by VALUED_1:11
.= (p1/.i - p2/.i)^2 by A6,A7,A1,A5,A4,VALUED_1:13;
hence thesis by A1,A2,A3,A5,A4,MATRPROB:5;
end;
theorem Th9:
for a, o, p being Element of TOP-REAL n st a in Ball(o,r) holds
for x being object holds |.(a-o).x.| < r & |.a.x-o.x.| < r
proof
let a, o, p be Element of TOP-REAL n;
assume
A1: a in Ball(o,r);
then
A2: |.a-o.| < r by TOPREAL9:7;
0 <= Sum sqr (a-o) by RVSUM_1:86;
then (sqrt Sum sqr (a-o))^2 = Sum sqr (a-o) by SQUARE_1:def 2;
then
A3: Sum sqr (a-o) < r^2 by A2,SQUARE_1:16;
A4: sqr(a-o) = sqr(o-a) by EUCLID:20;
A5: r > 0 by A1;
let x;
A6: dom(a-o) = dom a /\ dom o by VALUED_1:12;
A7: dom a = Seg n & dom o = Seg n by FINSEQ_1:89;
per cases;
suppose
A8: x in dom a;
then reconsider x as Nat;
A9: (a-o).x = a.x - o.x by A8,A6,A7,VALUED_1:13;
A10: a/.x = a.x & o/.x = o.x by A8,A7,PARTFUN1:def 6;
now
assume o.x - a.x >= r;
then
A11: (o.x - a.x)^2 >= r^2 by A5,SQUARE_1:15;
Sum sqr (o-a) >= (o/.x-a/.x)^2 by A8,A7,Th8;
hence contradiction by A3,A11,A4,A10,XXREAL_0:2;
end;
then
A12: o.x - r < a.x by XREAL_1:11;
now
assume a.x - o.x >= r;
then
A13: (a.x - o.x)^2 >= r^2 by A5,SQUARE_1:15;
Sum sqr (a-o) >= (a/.x-o/.x)^2 by A8,Th8;
hence contradiction by A3,A13,A10,XXREAL_0:2;
end;
then a.x < o.x + r by XREAL_1:19;
hence thesis by A9,A12,RINFSUP1:1;
end;
suppose
A14: not x in dom a;
then not x in dom abs(a-o) by A6,A7,VALUED_1:def 11;
then abs(a-o).x = 0 by FUNCT_1:def 2;
then
A15: |.(a-o).x.| = 0 by VALUED_1:18;
a.x = 0 & o.x = 0 by A7,A14,FUNCT_1:def 2;
hence thesis by A15,A1;
end;
end;
theorem Th10:
for a, o being Point of Euclid n st a in Ball(o,r) holds
for x being object holds |.(a-o).x.| < r & |.a.x-o.x.| < r
proof
let a, o be Point of Euclid n;
reconsider a1 = a, o1 = o as Point of TOP-REAL n by EUCLID:67;
A1: Ball(o,r) = Ball(o1,r) by TOPREAL9:13;
a-o = a1-o1;
hence thesis by A1,Th9;
end;
definition
let f be real-valued Function, r be Real;
func Intervals(f,r) -> Function means
:Def3:
dom it = dom f &
for x being object st x in dom f holds it.x = ].f.x-r,f.x+r.[;
existence
proof
deffunc F(object) = ].f.$1-r,f.$1+r.[;
ex g being Function st dom g = dom f &
for x being object st x in dom f holds g.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let g, h be Function such that
A1: dom g = dom f and
A2: for x being object st x in dom f holds g.x = ].f.x-r,f.x+r.[ and
A3: dom h = dom f and
A4: for x being object st x in dom f holds h.x = ].f.x-r,f.x+r.[;
now
let x be object;
assume
A5: x in dom g;
hence g.x = ].f.x-r,f.x+r.[ by A1,A2
.= h.x by A1,A4,A5;
end;
hence thesis by A1,A3,FUNCT_1:2;
end;
end;
registration
let r;
cluster Intervals({},r) -> empty;
coherence
proof
dom Intervals({},r) = dom {} by Def3;
hence thesis;
end;
end;
registration
let f be real-valued FinSequence; let r;
cluster Intervals(f,r) -> FinSequence-like;
coherence
proof
take len f;
dom Intervals(f,r) = dom f by Def3;
hence thesis by FINSEQ_1:def 3;
end;
end;
definition
let n, e, r;
func OpenHypercube(e,r) -> Subset of TopSpaceMetr Euclid n equals
product Intervals(e,r);
coherence
proof
set T = TopSpaceMetr Euclid n;
set f = Intervals(e,r);
product f c= the carrier of T
proof
let x be object;
assume x in product f;
then consider g being Function such that
A1: x = g and
A2: dom g = dom f and
A3: for y being object st y in dom f holds g.y in f.y by CARD_3:def 5;
A4: dom f = dom e by Def3;
dom e = Seg n by FINSEQ_1:89;
then reconsider x as FinSequence by A1,A2,A4,FINSEQ_1:def 2;
rng x c= REAL
proof
let b be object;
assume b in rng x;
then consider a being object such that
A5: a in dom x and
A6: x .a = b by FUNCT_1:def 3;
A7: g.a in f.a by A1,A2,A3,A5;
f.a = ].e.a-r,e.a+r.[ by A1,A2,A4,A5,Def3;
hence thesis by A1,A6,A7;
end;
then x is FinSequence of REAL by FINSEQ_1:def 4;
then
A8: x in REAL* by FINSEQ_1:def 11;
len e = n by CARD_1:def 7;
then len x = n by A1,A2,A4,FINSEQ_3:29;
hence thesis by A8;
end;
hence thesis;
end;
end;
theorem Th11:
0 < r implies e in OpenHypercube(e,r)
proof
assume
A1: 0 < r;
set f = Intervals(e,r);
A2: dom f = dom e by Def3;
now
let x be object;
assume x in dom f;
then
A3: f.x = ].e.x-r,e.x+r.[ by A2,Def3;
A4: e.x-r < e.x-0 by A1,XREAL_1:10;
e.x+0 < e.x+r by A1,XREAL_1:8;
hence e.x in f.x by A3,A4,XXREAL_1:4;
end;
hence thesis by A2,CARD_3:9;
end;
registration
let n be non zero Nat; let e be Point of Euclid n;
let r be non positive Real;
cluster OpenHypercube(e,r) -> empty;
coherence
proof
assume not thesis;
then consider x being object such that
A1: x in OpenHypercube(e,r);
reconsider e1 = e as real-valued Function;
set f = Intervals(e,r);
A2: dom f = dom e by Def3;
A3: dom e = Seg n by FINSEQ_1:89;
consider N being object such that
A4: N in Seg n by XBOOLE_0:def 1;
f.N = ].e1.N-r,e1.N+r.[ by A4,A3,Def3;
hence thesis by A1,A2,A3,A4,CARD_3:9;
end;
end;
theorem Th12:
for e being Point of Euclid 0 holds OpenHypercube(e,r) = {{}} by CARD_3:10;
registration
let e be Point of Euclid 0;
let r;
cluster OpenHypercube(e,r) -> non empty;
coherence by CARD_3:10;
end;
registration
let n, e; let r be positive Real;
cluster OpenHypercube(e,r) -> non empty;
coherence by Th11;
end;
theorem Th13:
r <= s implies OpenHypercube(e,r) c= OpenHypercube(e,s)
proof
assume
A1: r <= s;
A2: dom Intervals(e,s) = dom e by Def3;
A3: dom Intervals(e,r) = dom e by Def3;
now
let x be object;
assume
A4: x in dom Intervals(e,r);
reconsider u = e.x as Real;
A5: Intervals(e,r).x = ].u-r,u+r.[ & Intervals(e,s).x = ].u-s,u+s.[
by A4,A3,Def3;
u-s <= u-r & u+r <= u+s by A1,XREAL_1:6,10;
hence Intervals(e,r).x c= Intervals(e,s).x by A5,XXREAL_1:46;
end;
hence thesis by A2,A3,CARD_3:27;
end;
theorem Th14:
(n <> 0 or 0 < r) & e1 in OpenHypercube(e,r) implies
for x being set holds |.(e1-e).x.| < r & |.e1.x-e.x.| < r
proof
assume that
A1: n <> 0 or 0 < r and
A2: e1 in OpenHypercube(e,r);
A3: dom e1 = Seg n & dom e = Seg n by FINSEQ_1:89;
A4: dom(e1-e) = dom e1 /\ dom e by VALUED_1:12;
let x be set;
per cases;
suppose
A5: x in dom e1;
then
A6: (e1-e).x = e1.x-e.x by A3,A4,VALUED_1:13;
dom e = dom Intervals(e,r) by Def3;
then
A7: e1.x in Intervals(e,r).x by A5,A3,A2,CARD_3:9;
Intervals(e,r).x = ].e.x-r,e.x+r.[ by A3,A5,Def3;
hence thesis by A6,A7,FCONT_3:1;
end;
suppose
A8: not x in dom e1;
then not x in dom abs(e1-e) by A4,A3,VALUED_1:def 11;
then abs(e1-e).x = 0 by FUNCT_1:def 2;
then
A9: |.(e1-e).x.| = 0 by VALUED_1:18;
e1.x = 0 & e.x = 0 by A3,A8,FUNCT_1:def 2;
hence thesis by A9,A1,A2;
end;
end;
theorem Th15:
n <> 0 & e1 in OpenHypercube(e,r) implies Sum sqr (e1-e) < n*r^2
proof
assume that
A1: n <> 0 and
A2: e1 in OpenHypercube(e,r);
set R1 = sqr(e1-e);
set R2 = n|->(r^2);
A6: now
let i;
assume
A7: i in Seg n;
A8: dom e1 = Seg n & dom e = Seg n by FINSEQ_1:89;
dom(e1-e) = dom e1 /\ dom e by VALUED_1:12;
then
A9: (e1-e).i = e1.i-e.i by A7,A8,VALUED_1:13;
A10: R1.i = ((e1-e).i)^2 by VALUED_1:11;
A11: R2.i = r^2 by A7,FINSEQ_2:57;
A12: |.e1.i-e.i.| < r by A1,A2,Th14;
((e1-e).i)^2 = |.(e1-e).i.|^2 by COMPLEX1:75;
hence R1.i < R2.i by A9,A10,A11,A12,SQUARE_1:16;
end;
then
A13: for i st i in Seg n holds R1.i <= R2.i;
ex i st i in Seg n & R1.i < R2.i
proof
consider i being object such that
A14: i in Seg n by A1,XBOOLE_0:def 1;
reconsider i as Nat by A14;
take i;
thus thesis by A14,A6;
end;
then Sum R1 < Sum R2 by A13,RVSUM_1:83;
hence thesis by RVSUM_1:80;
end;
theorem Th16:
n <> 0 & e1 in OpenHypercube(e,r) implies dist(e1,e) < r * sqrt(n)
proof
assume that
A1: n <> 0 and
A2: e1 in OpenHypercube(e,r);
A3: dist(e1,e) = |.e1-e.| by EUCLID:def 6;
0 <= Sum sqr (e1-e) by RVSUM_1:86;
then
A4: sqrt Sum sqr (e1-e) < sqrt(n*r^2) by A1,A2,Th15,SQUARE_1:27;
0 <= r by A1,A2;
then sqrt(r^2) = r by SQUARE_1:22;
hence thesis by A3,A4,SQUARE_1:29;
end;
theorem Th17:
n <> 0 implies OpenHypercube(e,r/sqrt(n)) c= Ball(e,r)
proof
assume
A1: n <> 0;
let x be object;
assume
A2: x in OpenHypercube(e,r/sqrt(n));
then reconsider x as Point of Euclid n;
A3: dist(x,e) < r/sqrt(n)*sqrt(n) by A1,A2,Th16;
r/sqrt(n)*sqrt(n) = r by A1,XCMPLX_1:87;
hence thesis by A3,METRIC_1:11;
end;
theorem
n <> 0 implies OpenHypercube(e,r) c= Ball(e,r*sqrt(n))
proof
assume
A1: n <> 0;
then
A2: OpenHypercube(e,r*sqrt(n)/sqrt(n)) c= Ball(e,r*sqrt(n)) by Th17;
r/sqrt(n)*sqrt(n) = r by A1,XCMPLX_1:87;
hence thesis by A2,XCMPLX_1:74;
end;
theorem Th19:
e1 in Ball(e,r) implies
ex m being non zero Element of NAT st OpenHypercube(e1,1/m) c= Ball(e,r)
proof
reconsider B = Ball(e,r) as Subset of TopSpaceMetr Euclid n;
assume
A1: e1 in Ball(e,r);
B is open by TOPMETR:14;
then consider s being Real such that
A2: s > 0 and
A3: Ball(e1,s) c= B by A1,TOPMETR:15;
per cases;
suppose
A4: n <> 0;
then consider m being Nat such that
A5: 1/m < s/sqrt(n) and
A6: m > 0 by A2,FRECHET:36;
reconsider m as non zero Element of NAT by A6,ORDINAL1:def 12;
A7: OpenHypercube(e1,s/sqrt(n)) c= Ball(e1,s) by A4,Th17;
OpenHypercube(e1,1/m) c= OpenHypercube(e1,s/sqrt(n)) by A5,Th13;
then OpenHypercube(e1,1/m) c= Ball(e1,s) by A7;
hence thesis by A3,XBOOLE_1:1;
end;
suppose n = 0;
then (OpenHypercube(e1,1/1) = {} or OpenHypercube(e1,1/1) = {{}}) &
Ball(e,r) = {{}} by A1,EUCLID:77,ZFMISC_1:33;
hence thesis;
end;
end;
theorem Th20:
n <> 0 & e1 in OpenHypercube(e,r) implies r > abs(e1-e).max_diff_index(e1,e)
proof
set d = max_diff_index(e1,e);
abs(e1-e).d = |.(e1-e).d.| by VALUED_1:18;
hence thesis by Th14;
end;
theorem Th21:
OpenHypercube(e1,r-abs(e1-e).max_diff_index(e1,e)) c= OpenHypercube(e,r)
proof
set d = max_diff_index(e1,e);
set F = abs(e1-e);
set s = r-F.d;
A1: dom e1 = Seg n & dom e = Seg n by FINSEQ_1:89;
let y be Point of TopSpaceMetr Euclid n;
assume
A2: y in OpenHypercube(e1,s);
reconsider y as Point of Euclid n;
A3: dom y = dom Intervals(e1,s) by A2,CARD_3:9;
A4: dom Intervals(e1,s) = dom e1 by Def3;
then A5: dom y = dom Intervals(e,r) by A1,A3,Def3;
now
let x be object;
assume
A6: x in dom Intervals(e,r);
then
A7: Intervals(e,r).x = ].e.x-r,e.x+r.[ by A1,A3,A4,A5,Def3;
A8: Intervals(e1,s).x = ].e1.x-s,e1.x+s.[ by A3,A4,A5,A6,Def3;
y.x in Intervals(e1,s).x by A2,A3,A5,A6,CARD_3:9;
then
A9: |.y.x-e1.x.| < s by A8,RCOMP_1:1;
dom(e1-e) = dom e1 /\ dom e by VALUED_1:12;
then |.e1.x-e.x.|= |.(e1-e).x.| by A1,A3,A4,A5,A6,VALUED_1:13
.= abs(e1-e).x by VALUED_1:18;
then
A10: |.y.x-e1.x.| + |.e1.x-e.x.| < s + F.d by A9,Th5,XREAL_1:8;
|.y.x-e.x.| <= |.y.x-e1.x.| + |.e1.x-e.x.| by COMPLEX1:63;
then |.y.x-e.x.| < r by A10,XXREAL_0:2;
hence y.x in Intervals(e,r).x by A7,RCOMP_1:1;
end;
hence thesis by A5,CARD_3:9;
end;
theorem Th22:
Ball(e,r) c= OpenHypercube(e,r)
proof
let g be object;
assume
A1: g in Ball(e,r);
then reconsider g as Point of Euclid n;
A2: dom Intervals(e,r) = dom e by Def3;
A3: dom g = Seg n & dom e = Seg n by FINSEQ_1:89;
now
let x be object;
reconsider u = e.x, v = g.x as Real;
assume
A4: x in dom Intervals(e,r);
then
A5: Intervals(e,r).x = ].u-r,u+r.[ by A2,Def3;
dom(g-e) = dom g /\ dom e by VALUED_1:12;
then
A6: (g-e).x = v-u by A2,A3,A4,VALUED_1:13;
A7: v = u + (v-u);
|.(g-e).x.| < r by A1,Th10;
hence g.x in Intervals(e,r).x by A6,A5,A7,FCONT_3:3;
end;
hence thesis by A2,A3,CARD_3:9;
end;
registration
let n, e, r;
cluster OpenHypercube(e,r) -> open;
coherence
proof
per cases;
suppose
A1: n <> 0;
for p being Point of Euclid n st p in OpenHypercube(e,r)
ex s being Real st s > 0 & Ball(p,s) c= OpenHypercube(e,r)
proof
let p be Point of Euclid n;
assume
A2: p in OpenHypercube(e,r);
set d = abs(p-e).max_diff_index(p,e);
take s = r-d;
r-d > d-d by A1,A2,Th20,XREAL_1:8;
hence s > 0;
A3: OpenHypercube(p,s) c= OpenHypercube(e,r) by Th21;
Ball(p,s) c= OpenHypercube(p,s) by Th22;
hence Ball(p,s) c= OpenHypercube(e,r) by A3;
end;
hence thesis by TOPMETR:15;
end;
suppose
A4: n = 0;
then OpenHypercube(e,r) = {{}} by Th12;
then OpenHypercube(e,r) in the topology of TopSpaceMetr Euclid 0
by Th6,TARSKI:def 2;
hence thesis by A4,PRE_TOPC:def 2;
end;
end;
end;
theorem
for V being Subset of TopSpaceMetr Euclid n holds V is open implies
for e being Point of Euclid n st e in V
ex m being non zero Element of NAT st OpenHypercube(e,1/m) c= V
proof
let V be Subset of TopSpaceMetr Euclid n;
assume
A1: V is open;
let e be Point of Euclid n;
assume e in V;
then consider r being Real such that
A2: r > 0 and
A3: Ball(e,r) c= V by A1,TOPMETR:15;
consider m being non zero Element of NAT such that
A4: OpenHypercube(e,1/m) c= Ball(e,r) by A2,Th19,GOBOARD6:1;
take m;
thus thesis by A3,A4;
end;
theorem
for V being Subset of TopSpaceMetr Euclid n st
for e being Point of Euclid n st e in V
ex r being Real st r > 0 & OpenHypercube(e,r) c= V
holds V is open
proof
let V be Subset of TopSpaceMetr Euclid n;
assume
A1: for e being Point of Euclid n st e in V
ex r being Real st r > 0 & OpenHypercube(e,r) c= V;
for e be Point of Euclid n st e in V
ex r being Real st r > 0 & Ball(e,r) c= V
proof
let e be Point of Euclid n;
assume e in V;
then consider r being Real such that
A2: r > 0 and
A3: OpenHypercube(e,r) c= V by A1;
Ball(e,r) c= OpenHypercube(e,r) by Th22;
hence thesis by A2,A3,XBOOLE_1:1;
end;
hence thesis by TOPMETR:15;
end;
deffunc K(Nat,Point of Euclid $1) =
the set of all OpenHypercube($2,1/m) where m is non zero Element of NAT;
definition
let n, e;
func OpenHypercubes(e) -> Subset-Family of TopSpaceMetr Euclid n equals
the set of all OpenHypercube(e,1/m) where m is non zero Element of NAT;
coherence
proof
K(n,e) c= bool the carrier of TopSpaceMetr Euclid n
proof
let x be object;
assume x in K(n,e);
then ex m being non zero Element of NAT st x = OpenHypercube(e,1/m);
hence thesis by ZFMISC_1:def 1;
end;
hence thesis;
end;
end;
registration
let n, e;
cluster OpenHypercubes(e) -> non empty open @e-quasi_basis;
coherence
proof
set T = TopSpaceMetr Euclid n;
OpenHypercube(e,1/1) in OpenHypercubes(e);
hence OpenHypercubes(e) is non empty;
hereby
let A be Subset of T;
assume A in OpenHypercubes(e);
then ex m being non zero Element of NAT st A = OpenHypercube(e,1/m);
hence A is open;
end;
now
let Y be set;
assume Y in OpenHypercubes(e);
then ex m being non zero Element of NAT st Y = OpenHypercube(e,1/m);
hence @e in Y by Th11;
end;
hence @e in Intersect OpenHypercubes(e) by SETFAM_1:43;
let S be Subset of T such that
A1: S is open and
A2: @e in S;
consider r being Real such that
A3: r > 0 and
A4: Ball(e,r) c= S by A1,A2,TOPMETR:15;
consider m being non zero Element of NAT such that
A5: OpenHypercube(e,1/m) c= Ball(e,r) by A3,Th19,GOBOARD6:1;
take V = OpenHypercube(e,1/m);
thus V in OpenHypercubes(e);
thus V c= S by A4,A5;
end;
end;
Lm1: now
set J = {} --> R^1;
set C = Carrier J;
set P = product J;
set T = TopSpaceMetr Euclid 0;
A1: the carrier of P = product C by WAYBEL18:def 3;
A2: product {} = {{}} by CARD_3:10;
A3: REAL 0 = {0. TOP-REAL 0} by EUCLID:77;
A4: {the carrier of T} is Basis of T by YELLOW_9:10;
the carrier of T = the carrier of P by A1,A2,A3;
then P is 1-element;
then {the carrier of P} is Basis of P by YELLOW_9:10;
hence T = P by A1,A2,A3,A4,YELLOW_9:25;
end;
theorem Th25:
Funcs(Seg n,REAL) = product Carrier (Seg n --> R^1)
proof
set J = Seg n --> R^1;
set C = Carrier J;
A1: dom C = Seg n by PARTFUN1:def 2;
thus Funcs(Seg n,REAL) c= product C
proof
let f be object;
assume f in Funcs(Seg n,REAL);
then reconsider f as Function of Seg n,REAL by FUNCT_2:66;
A2: dom f = Seg n by FUNCT_2:def 1;
now
let x be object;
assume
A3: x in dom C;
then
A4: ex R being 1-sorted st R = J.x & C.x = the carrier of R
by PRALG_1:def 15;
f.x in REAL by A3,FUNCT_2:5;
hence f.x in C.x by A4,A3,FUNCOP_1:7;
end;
hence thesis by A2,A1,CARD_3:9;
end;
let x be object;
assume x in product C;
then consider g being Function such that
A5: x = g and
A6: dom g = dom C and
A7: for y being object st y in dom C holds g.y in C.y by CARD_3:def 5;
rng g c= REAL
proof
let z be object;
assume z in rng g;
then consider a being object such that
A8: a in dom g and
A9: g.a = z by FUNCT_1:def 3;
A10: ex R being 1-sorted st R = J.a & C.a = the carrier of R
by A6,A8,PRALG_1:def 15;
J.a = R^1 by A6,A8,FUNCOP_1:7;
hence thesis by A6,A7,A8,A9,A10;
end;
hence thesis by A1,A5,A6,FUNCT_2:def 2;
end;
theorem Th26:
n <> 0 implies for PP being Subset-Family of TopSpaceMetr Euclid n st
PP = product_prebasis (Seg n --> R^1) holds PP is quasi_prebasis
proof
assume
A1: n <> 0;
set E = Euclid n;
set T = TopSpaceMetr E;
let PP be Subset-Family of T;
set J = Seg n --> R^1;
set C = Carrier J;
set S = Seg n;
reconsider S as non empty finite set by A1;
assume
A2: PP = product_prebasis (Seg n --> R^1);
A3: REAL n = Funcs(Seg n,REAL) by FINSEQ_2:93;
A4: dom C = Seg n by PARTFUN1:def 2;
A5: Funcs(Seg n,REAL) = product C by Th25;
defpred P[set,object] means ex e being Point of E st e = $1 &
$2 = OpenHypercubes(e);
A6: for i being Element of T ex j being object st P[i,j]
proof
let i be Element of T;
reconsider j = i as Point of E;
take OpenHypercubes(j),j;
thus thesis;
end;
consider NS being ManySortedSet of T such that
A7: for x being Point of T holds P[x,NS.x] from PBOOLE:sch 6(A6);
now
let x be Point of T;
reconsider y = x as Point of E;
P[y,NS.y] by A7;
hence NS.x is Basis of x;
end;
then reconsider NS as Neighborhood_System of T by TOPGEN_2:def 3;
take B = Union NS;
let b be object;
reconsider bb=b as set by TARSKI:1;
assume b in B;
then consider Z being set such that
A8: b in Z and
A9: Z in rng NS by TARSKI:def 4;
consider x being object such that
A10: x in dom NS and
A11: NS.x = Z by A9,FUNCT_1:def 3;
reconsider x as Point of E by A10;
A12: dom x = Seg n by FINSEQ_1:89;
P[x,NS.x] by A7;
then consider m being non zero Element of NAT such that
A13: b = OpenHypercube(x,1/m) by A8,A11;
deffunc A(object) = product(C+*($1,R^1(].x .$1-1/m,x .$1+1/m.[)));
defpred R[set] means not contradiction;
set Y = {A(q) where q is Element of S : R[q]};
A14: Y is finite from PRE_CIRC:sch 1;
Y c= bool the carrier of T
proof
let s be object;
assume s in Y;
then consider q being Element of S such that
A15: s = A(q);
A(q) c= the carrier of T
proof
let z be object;
set f = C+*(q,R^1(].x .q-1/m,x .q+1/m.[));
assume z in A(q);
then consider g being Function such that
A16: z = g and
A17: dom g = dom f and
A18: for d being object st d in dom f holds g.d in f.d by CARD_3:def 5;
A19: dom f = dom C by FUNCT_7:30;
then reconsider g as FinSequence by A4,A17,FINSEQ_1:def 2;
rng g c= REAL
proof
let b be object;
assume b in rng g;
then consider a being object such that
A20: a in dom g and
A21: g.a = b by FUNCT_1:def 3;
A22: g.a in f.a by A17,A18,A20;
per cases;
suppose a = q;
then f.a = R^1(].x .q-1/m,x .q+1/m.[) by A17,A19,A20,FUNCT_7:31;
hence thesis by A21,A22;
end;
suppose a <> q;
then
A23: f.a = C.a by FUNCT_7:32;
ex R being 1-sorted st R = J.a & C.a = the carrier of R
by A20,A17,A19,PRALG_1:def 15;
hence thesis by A21,A22,A23,A20,A17,A19,FUNCOP_1:7;
end;
end;
then g is FinSequence of REAL by FINSEQ_1:def 4;
then
A24: g is Element of REAL* by FINSEQ_1:def 11;
n in NAT by ORDINAL1:def 12;
then len g = n by A4,A17,A19,FINSEQ_1:def 3;
hence thesis by A16,A24;
end;
hence thesis by A15,ZFMISC_1:def 1;
end;
then reconsider Y as Subset-Family of T;
A25: Y c= PP
proof
let z be object;
assume
A26: z in Y;
then consider i being Element of S such that
A27: z = A(i);
J.i = R^1;
hence thesis by A2,A5,A26,A3,A27,WAYBEL18:def 2;
end;
consider N being object such that
A28: N in S by XBOOLE_0:def 1;
A29: A(N) in Y by A28;
then
A30: Intersect Y = meet Y by SETFAM_1:def 9;
A31: dom Intervals(x,1/m) = dom x by Def3;
A32:
now
let i be Element of S;
set f = C+*(i,R^1(].x .i-1/m,x .i+1/m.[));
thus product Intervals(x,1/m) c= product f
proof
let d be object;
assume d in product Intervals(x,1/m);
then consider d1 being Function such that
A33: d = d1 and
A34: dom d1 = dom Intervals(x,1/m) and
A35: for a being object st a in dom Intervals(x,1/m) holds
d1.a in Intervals(x,1/m).a by CARD_3:def 5;
A36: dom f = dom C by FUNCT_7:30;
now
let k be object;
assume
A37: k in dom f;
then
A38: Intervals(x,1/m).k = ].x .k-1/m,x .k+1/m.[ by A36,A12,Def3;
A39: d1.k in Intervals(x,1/m).k by A35,A31,A12,A36,A37;
per cases;
suppose k = i;
hence d1.k in f.k by A38,A39,A37,A36,FUNCT_7:31;
end;
suppose k <> i;
then
A40: f.k = C.k by FUNCT_7:32;
A41: ex R being 1-sorted st R = J.k & C.k = the carrier of R
by A37,A36,PRALG_1:def 15;
d1.k in REAL by A38,A39;
hence d1.k in f.k by A40,A41,A37,A36,FUNCOP_1:7;
end;
end;
hence d in product f by A33,A4,A34,A31,A12,A36,CARD_3:9;
end;
end;
bb = Intersect Y
proof
now
let M be set;
assume M in Y;
then ex i being Element of S st M = A(i);
hence bb c= M by A13,A32;
end;
hence bb c= Intersect Y by A30,A29,SETFAM_1:5;
let q be object;
assume
A42: q in Intersect Y;
then reconsider q as Function;
A43: dom q = Seg n by A42,FINSEQ_1:89;
now
let a be object such that
A44: a in dom Intervals(x,1/m);
A45: Intervals(x,1/m).a = ].x .a-1/m,x .a+1/m.[ by A44,A31,Def3;
set f = C+*(a,R^1(].x .a-1/m,x .a+1/m.[));
A(a) in Y by A44,A31,A12;
then
A46: q in A(a) by A42,SETFAM_1:43;
then
A47: dom q = dom f by CARD_3:9;
then
A48: q.a in f.a by A43,A44,A31,A12,A46,CARD_3:9;
dom f = dom C by FUNCT_7:30;
hence q.a in Intervals(x,1/m).a
by A45,A48,A43,A44,A31,A12,A47,FUNCT_7:31;
end;
hence thesis by A13,A43,A31,A12,CARD_3:9;
end;
hence thesis by A25,A14,CANTOR_1:def 3;
end;
theorem Th27:
for PP being Subset-Family of TopSpaceMetr Euclid n st
PP = product_prebasis (Seg n --> R^1) holds PP is open
proof
let PP be Subset-Family of TopSpaceMetr Euclid n;
set J = Seg n --> R^1;
set C = Carrier J;
set T = TopSpaceMetr Euclid n;
set E = Euclid n;
assume
A1: PP = product_prebasis (Seg n --> R^1);
let x be Subset of T;
assume x in PP;
then consider i being set, R being TopStruct, V being Subset of R
such that
A2: i in Seg n and
A3: V is open and
A4: R = J.i and
A5: x = product (C +* (i,V)) by A1,WAYBEL18:def 2;
A6: dom C = Seg n by PARTFUN1:def 2;
A7: now
let i be set;
let e, y be Point of E;
let r be Real;
assume
A8: y in Ball(e,r);
set O = ].e.i-r, e.i+r.[;
set G = C +* (i,O);
A9: dom y = Seg n by FINSEQ_1:89;
A10: dom G = dom C by FUNCT_7:30;
now
let a be object;
assume
A11: a in dom G;
per cases;
suppose
A12: a = i;
A13: y.i = e.i + (y.i-e.i);
A14: dom e = Seg n by FINSEQ_1:89;
dom(y-e) = dom y /\ dom e by VALUED_1:12;
then
A15: (y-e).i = y.i-e.i by A9,A14,A11,A12,A10,VALUED_1:13;
|.(y-e).i.| < r by A8,Th10;
then y.i in O by A15,A13,FCONT_3:3;
hence y.a in G.a by A12,A10,A11,FUNCT_7:31;
end;
suppose a <> i;
then
A16: G.a = C.a by FUNCT_7:32;
A17: ex R being 1-sorted st R = J.a & C.a = the carrier of R
by A11,A10,PRALG_1:def 15;
y.a in REAL by XREAL_0:def 1;
hence y.a in G.a by A16,A11,A10,A17,FUNCOP_1:7;
end;
end;
hence y in product G by A10,A6,A9,CARD_3:9;
end;
set F = C +* (i,V);
A18: R = R^1 by A2,A4,FUNCOP_1:7;
for e being Element of E st e in x
ex r being Real st r > 0 & Ball(e,r) c= x
proof
let e be Element of E;
assume
A19: e in x;
A20: dom F = dom C by FUNCT_7:30;
then
A21: e.i in F.i by A2,A6,A19,A5,CARD_3:9;
A22: F.i = V by A2,A6,FUNCT_7:31;
then consider r being Real such that
A23: r > 0 and
A24: ].e.i-r, e.i+r.[ c= V by A3,A18,A21,FRECHET:8;
take r;
thus r > 0 by A23;
let y be object;
assume
A25: y in Ball(e,r);
then reconsider y as Point of E;
set O = ].e.i-r, e.i+r.[;
set G = C +* (i,O);
A26: dom G = dom C by FUNCT_7:30;
A27: y in product G by A25,A7;
now
let a be object;
assume
A28: a in dom G;
per cases;
suppose a = i;
hence G.a c= F.a by A24,A22,A26,A28,FUNCT_7:31;
end;
suppose a <> i;
then G.a = C.a & F.a = C.a by FUNCT_7:32;
hence G.a c= F.a;
end;
end;
then product G c= product F by A20,CARD_3:27,FUNCT_7:30;
hence thesis by A27,A5;
end;
then x in the topology of T by PCOMPS_1:def 4;
hence thesis by PRE_TOPC:def 2;
end;
theorem
TopSpaceMetr Euclid n = product(Seg n --> R^1)
proof
set J = Seg n --> R^1;
per cases;
suppose
A1: n = 0;
then J = {} --> R^1;
hence thesis by A1,Lm1;
end;
suppose
A2: n <> 0;
A3: REAL n = Funcs(Seg n,REAL) by FINSEQ_2:93;
A4: Funcs(Seg n,REAL) = product Carrier J by Th25;
then reconsider PP = product_prebasis J as
Subset-Family of TopSpaceMetr Euclid n by FINSEQ_2:93;
A5: PP is open by Th27;
PP is quasi_prebasis by A2,Th26;
hence thesis by A4,A3,A5,WAYBEL18:def 3;
end;
end;